nat_compl:

Add and prove lt_ltn, le_leq.

ord_compl:
WIP: map_injS_uniq.
Add def in_ordS.
Add and prove nth_ord_enum_alt,
              in_ordS_correct_{l{,_alt},r}, val_in_ordS, in_ordS_injS,
              ord_enumS_eq.
Proof of perm_ord_enum_sort.

Finite_family:
Simplify proof.