proposition: Lemma inverse_order_is r r' f: order_isomorphism f r r' -> order_isomorphism (inverse_fun f) r' r.
proof: Proof. rewrite /order_isomorphism. move=>[or or' [bf sf tf] fp];saw. by split; aw => //; apply: inverse_bij_fb. move=> x y xt yt. move: (xt)(yt); aw => xt1 yt1. rewrite -{1} (inverse_V bf xt1) -{1} (inverse_V bf yt1). have aux: (source f = target (inverse_fun f)) by aw. move: (inverse_bij_fb bf) => [[fi _] _]. symmetry;apply/fp; rewrite aux; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)