proposition: Lemma EP_fun_pr: order_isomorphism EP_fun r1 r2.
proof: Proof. have [bf sf tf] := bij_f. have [bg sg tg] := bij_g. have tor1: total_order r1 by move:eta_like_r1 => [[]]. have or2: order r2 by move:eta_like_r2 => [[[]]]. have sra: substrate r1 = source EP_fun by rewrite /EP_fun; aw. have srb: substrate r2 = target EP_fun by rewrite /EP_fun; aw. have ifb:=(inverse_bij_fb bf). have [bh sh th] := EPfun_aux_bij. have aa: g \coP EPfun_aux by split; try fct_tac; rewrite th. have b1: bijection (g \co EPfun_aux) by apply:compose_fb => //. have co1: (g \co EPfun_aux) \coP inverse_fun f. by split ; try fct_tac; aw; rewrite sh. have bH:bijection EP_fun by apply: compose_fb. apply: total_order_isomorphism => //. rewrite - sra - tf => x y xsr ysr lexy. have tif: target (inverse_fun f) = (source EPfun_aux) by rewrite sh; aw. have ff:=(proj1 (proj1 ifb)). have xsf: inc (Vf (inverse_fun f) x) (source EPfun_aux) by Wtac; aw. have ysf: inc (Vf (inverse_fun f) y) (source EPfun_aux) by Wtac; aw. have nx: natp (Vf (inverse_fun f) x) by rewrite /natp - sh. have ny: natp (Vf (inverse_fun f) y) by rewrite /natp - sh. case: (equal_or_not x y) => exy. by rewrite exy; order_tac; Wtac; [ fct_tac |rewrite - sra -tf]. have [//]: glt r2 (Vf EP_fun x) (Vf EP_fun y). rewrite /EP_fun !compfV //; aw; trivial; apply /EPfun_aux_M => //. by rewrite inverse_V // inverse_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)