proposition: Lemma Exercise1_3a15: E13_H1 -> E13_H2 -> order_isomorphism (fun_on_quotient E13_S E13_lam) (quotient_order E13_F E13_S) r.
proof: Proof. move=> h1 h2; move: (Exercise1_3a14 h1 h2) => [pa pb pc pd]. have gg:= Exercise1_3a1. have oo: (order (order_sum r g)) by fprops. have bf:= Exercise1_3a13. suff : (order_morphism (fun_on_quotient E13_S E13_lam) (quotient_order E13_F (equivalence_associated E13_lam)) r). by move => [p1 p2 [p3 p4 p5] p6]; split => //; split => //; apply: bf. by rewrite Exercise1_2f3; [| apply: Exercise1_3a4 =>// | apply: Exercise1_3a10 | apply: Exercise1_3a11]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)