proposition: Lemma Exercise1_3a14: E13_H1 -> E13_H2 -> [/\ Ex1_2_hC E13_F E13_S, Ex1_2_hC' E13_F E13_S, Ex1_2_hD E13_F E13_lam & Ex1_2_hD' E13_F r E13_lam].
proof: Proof. move=> h1 h2. move: (orsum_sr h1); rewrite -/E13_sF -/E13_F => s1. move: (orsum_or h1) => o1. have pa: Ex1_2_hC E13_F E13_S. move => x y z r1 /Exercise1_3a6P [xs sz qxz]. have ys: inc y E13_sF by rewrite - s1; order_tac. case: (equal_or_not (Q x) (Q y)) => qxy. exists z; last by order_tac; rewrite s1. apply /Exercise1_3a6P;split => //; ue. exists y; first by apply /Exercise1_3a6P. apply /orsum_gleP; split => //; left; rewrite -qxz; split; last by exact. exact (orsum_gle_id h1 r1). have pb:Ex1_2_hC' E13_F E13_S. move => x y z r1 r2. move: (orsum_gle_id h1 r1) (orsum_gle_id h1 r2) => q1 q2. move: r1 r2 => /orsum_gleP [_ ys _] _ /Exercise1_3a6P [xs _ sq]. apply /Exercise1_3a6P; split => //; move: h1 => [or _ _]. rewrite - sq in q2; order_tac. have ww: source E13_lam = E13_sF by rewrite /E13_lam /second_proj; aw. rewrite /Ex1_2_hD /Ex1_2_hD' ww. split => //. move=> x y x' => /orsum_gleP [xs ys lexy] x's. have r1: (Vf E13_lam x = Q x) by rewrite /E13_lam second_proj_V. have r2: (Vf E13_lam x' = Q x') by rewrite /E13_lam second_proj_V. have r3: (Vf E13_lam y = Q y) by rewrite /E13_lam second_proj_V. rewrite r1 r2 r3;move=> sq; case: lexy. rewrite sq; move=> lt; exists y;split => //; apply /orsum_gleP. by split => //; left. move=> [p1 p2]; exists x'; split => //; last by rewrite r2 - sq -p1. order_tac; ue. move => x y xs ys lxy. exists x; case: (equal_or_not (Vf E13_lam x) (Vf E13_lam y)) => h. exists x; split => //; order_tac; rewrite orsum_sr //. exists y; split => //; apply /orsum_gleP; split => //; left. move: lxy h;rewrite /E13_lam !second_proj_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)