proposition: Theorem finite_ordered_interval1 r: total_order r -> finite_set (substrate r) -> exists !f, order_isomorphism f r (Nint_co (cardinal (substrate r))).
proof: Proof. move=> tor fs. move/NatP: (fs) => fs'. have wor := (finite_set_torder_wor tor fs). move /card_eqP:(card_Nint fs'); rewrite - (proj2 (Nintco_wor _)) => /EqS e. have tor' := (worder_total (proj1(Nintco_wor (cardinal (substrate r))))). by apply: (isomorphism_worder_finite tor tor' fs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)