proposition: Lemma order_isomorphism_P f r r': order r -> order r' -> bijection f -> substrate r = source f -> substrate r' = target f -> (order_isomorphism f r r' <-> (increasing_fun f r r' /\ increasing_fun (inverse_fun f) r' r)).
proof: Proof. move=> or or' bf sr sr'. move: (bijective_inv_f bf)=> bif. have sf: source f = target (inverse_fun f) by rewrite /inverse_fun; aw. have tf: target f = source (inverse_fun f) by rewrite /inverse_fun; aw. split. move => h; move:(order_isomorphism_incr h) => h2. split; saw. - split=> //; fct_tac. - split; aw => //; fct_tac. - move=>x y rxy. have xt: inc x (target f) by rewrite - sr'; order_tac. have yt: inc y (target f) by rewrite - sr'; order_tac. by apply /(proj44 h); try Wtac; rewrite (inverse_V bf xt) (inverse_V bf yt). move=> [inf inif]; hnf; split => // x y xsf ysf. split; first by move=> hy; apply: (proj44 inf). move=> hyp. rewrite - (inverse_V2 bf xsf) - (inverse_V2 bf ysf). by apply: (proj44 inif). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)