proposition: Lemma Exercise1_3a4: E13_H1 -> E13_H2 -> increasing_fun E13_lam E13_F r.
proof: Proof. move=> h1 h2; move:(h1) => [p2 p3 p4]; split => //. + exact: (orsum_or h1). + split. * exact: Exercise1_3a0. * by rewrite (orsum_sr h1) /E13_lam /second_proj /E13_F; aw. * by rewrite -(Exercise1_3a3 h2). + move=> x y h3; move: (orsum_gle_id h1 h3). move: h3 => /orsum_gleP [xs ys xy] h4. rewrite / E13_lam second_proj_V // second_proj_V //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)