proposition: Theorem finite_ordered_interval r: total_order r -> finite_set (substrate r) -> exists! f, order_isomorphism f r (Nint_cco \1c (cardinal (substrate r))).
proof: Proof. move=> tot fs. move/NatP: (fs) => fs'. have [pa pb] := (Ninto_wor \1c (cardinal (substrate r))). move /card_eqP:(card_Nint1c fs') ;rewrite /Nint1c - pb => /EqS h. by apply: (isomorphism_worder_finite tot (worder_total pa) fs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)