proposition: Lemma Exercise1_6m': (increasing_mappings_order (order_product2 r r') r'') \Is (increasing_mappings_order r (increasing_mappings_order r' r'')).
proof: Proof. case: (p_or_not_p (nonempty E /\ nonempty F)) => H. move: H => [pa pb]; exists (second_partial_map2 r r' r''). by apply: Exercise1_6m. have esa: (E \times F) = emptyset. case: (emptyset_dichot E); first by move => ->; rewrite setX_0l. case: (emptyset_dichot F);first by move => ->; rewrite setX_0r. by move => n1 n2; case: H. have: (substrate (order_product2 r r')) = emptyset. by rewrite (order_product2_sr or or'). have: order (order_product2 r r') by apply: order_product2_or. set r3:= (order_product2 r r'). move => or3 sr3. case: (imo_osr r' or'');set r2 := (increasing_mappings_order r' r'') => or2 sr2. have [or4 sr4]:= (imo_osr r3 or''). have [or5 sr5]:= (imo_osr r or3). have [or6 sr6]:= (imo_osr r or2). have ssa:= functions_empty. have ssb: forall ra rb, order ra -> order rb -> substrate ra = emptyset -> substrate (increasing_mappings_order ra rb) = singleton (empty_function_tg (substrate rb)). move => ra rb ora orb h. rewrite (proj2 (imo_osr _ orb)) /increasing_mappings h. rewrite (ssa (substrate rb)). move:(empty_function_tg_function (substrate rb)) => [wa wb wc]. set_extens t; first by case /Zo_P. move => ta; apply: Zo_i => //; move /set1_P:ta => ->;split => //. split => //;ue. move => x y le. have: inc x (substrate ra) by order_tac. by rewrite h => /in_set0. move: (ssb _ _ or3 or'' sr3). set f0 := (empty_function_tg G); move => ssrc. have si: singletonp (substrate (increasing_mappings_order r r2)). case: (emptyset_dichot E) => h. rewrite (ssb _ _ or or2 h). by exists (empty_function_tg (substrate r2)). case: (emptyset_dichot F) => h1; last by case: H;split => //. rewrite sr6. move: (ssb _ _ or' or'' h1). set f1:= (empty_function_tg G) => sr2'. set f := Lf (fun _ => f1) E (substrate r2). have ta: lf_axiom (fun _ => f1) E (substrate r2). move => t _ ; rewrite sr2'; fprops. have ff: function f by apply: lf_function. exists f; apply :set1_pr. rewrite /f;apply: Zo_i; first by apply/functionsP;saw. split => //; first by saw. move => x y lexy; rewrite /E !LfV//; order_tac;rewrite sr2'; fprops. move =>t /Zo_P [] /functionsP [ft st tt] _; rewrite /f. apply: function_exten; aw; trivial; rewrite /E => x xst /=; rewrite LfV//; last by ue. by move: (Vf_target ft xst); rewrite tt sr2' => /set1_P ->. move: si => [w ws]. have ta: lf_axiom (fun _ => w) (singleton f0) (singleton w). move => t _ /=; fprops. exists (Lf (fun z => w) (singleton f0)(singleton w)). split => //. saw; try ue; apply: lf_bijective. + done. + by move => u v /set1_P -> /set1_P ->. + move => y /set1_P ->; exists f0;fprops. move => x y; rewrite lf_source; move => pa pb; aw. move: pa pb => /set1_P -> /set1_P ->;split => h; order_tac. rewrite ws !LfV//;fprops. rewrite ssrc; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)