proposition: Lemma isomorphism_worder_finite r r': total_order r -> total_order r' -> finite_set (substrate r) -> (substrate r) \Eq (substrate r') -> exists! f, order_isomorphism f r r'.
proof: Proof. move=> tor tor' fs /card_eqP => sc. have fs': finite_set (substrate r') by hnf; rewrite - sc. move:(finite_set_torder_wor tor fs) (finite_set_torder_wor tor' fs'). have aux: forall u v f, order_isomorphism f u v -> segmentp v (Imf f) /\ order_morphism f u v. move => f u v h; split; last by apply:order_isomorphism_w. move: h => [_ or' [[injf sjf] sf tf] pf]. by rewrite (surjective_pr0 sjf) tf; apply: substrate_segment. move => wor wor'; case: (isomorphism_worder_exists wor wor'). move => [f [pa mf]]; exists f; split. move: (order_morphism_fi mf) => injf. move: mf => [o1 o2 [ff sf tf] pf]; split => //; split => //. by apply: bijective_if_same_finite_c_inj; [ by rewrite sf tf | ue| exact]. by move => f'/aux [qa qb]; apply:(isomorphism_worder_unique wor wor'). move => [f [pa mf]]. have oi: (order_isomorphism f r' r). move: (order_morphism_fi mf) => injf. move: mf => [o1 o2 [ff sf tf] pf]. have bf: bijection f by apply: bijective_if_same_finite_c_inj; rewrite ? sf ?tf;[ symmetry; apply: sc| exact| exact]. split=> //. move: (inverse_order_is oi)=> oii. exists (inverse_fun f); split => // f' h1. move: (aux _ _ _ (inverse_order_is h1)) => [sa sb]. move: h1 => [_ _ [[[ff _] _] _ _] _ ]. by rewrite(isomorphism_worder_unique wor' wor pa sa mf sb)(ifun_involutive ff). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)