proposition: Lemma total_order_isomorphism f r r': total_order r -> order r' -> bijection f -> substrate r = source f -> substrate r' = target f -> {inc source f &, fincr_prop f r r'} -> order_isomorphism f r r'.
proof: Proof. move=> to or' bjf sf tf incf. move: (bjf) => [injf _]. have: (order_morphism f r r') by apply: total_order_morphism. by move=> [p1 p2 [p3 p4 p5] p6]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)