proposition: Lemma Exercise1_6l: nonempty E -> nonempty F -> bijection_prop (second_partial_map2 r r' r'' ) (increasing_mappings (order_product2 r r') r'') (increasing_mappings r (increasing_mappings_order r' r'')).
proof: Proof. move=> ne1 ne2. rewrite /second_partial_map2;saw. have op:=(order_product2_or or or'). have sop:=(order_product2_sr or or'). apply: lf_bijective. by apply: Exercise1_6k. move=> u v /soimP [[fu su tu] iu] /soimP [[fv sv tv] iv] sr. apply: function_exten => //; try ue. move: su sv; rewrite sop -/E -/F => su sv x xsu. have axu: inc u (functions (E \times F) G) by apply/functionsP. have axv: inc v (functions (E \times F) G) by apply/functionsP. move: (Exercise1_6h ne1 ne2 iu) => [dsu rsu]. move: (Exercise1_6h ne1 ne2 iv) => [dsv rsv]. have ssp: (second_partial_function G E F u = second_partial_function G E F v). apply: function_exten. + by apply: spfa_f. + by apply: spfa_f. + by rewrite /second_partial_function; aw; ue. + by rewrite /second_partial_function; aw; trivial; rewrite rsu rsv tu tv. + move=> a; rewrite lf_source => au. transitivity (Vf (restriction2 (second_partial_function G E F u) E (increasing_mappings r' r'')) a); [ | rewrite sr]; rewrite restriction2_V //; apply: Exercise1_6j => //. move: (xsu); rewrite su; move /setX_P => [px Ps Qr]. move: (spfa_V axu Ps) (spf_V axu Ps Qr); rewrite px => <- <-. move: (spfa_V axv Ps) (spf_V axv Ps Qr); rewrite px => <- <-; ue. move: (imo_osr r' or'') => [o2 sr2]. move=> y /soimP [[fy sy ty] incy]. have ta: (lf_axiom (fun z => Vf (Vf y (P z)) (Q z) ) (E \times F) G). move => t /setX_P; rewrite /E - sy; move=> [prt Pt Qt]. move: (Vf_target fy Pt); rewrite ty sr2 /G //. move /soimP => [[fw sw <-] _]; Wtac; ue. set (g:= Lf (fun z => Vf (Vf y (P z)) (Q z) ) (E \times F) G). have fg: function g by apply: lf_function. have ig: (increasing_fun g (order_product2 r r') r''). split => //; first by split;[done | rewrite /g; aw | rewrite /g; aw ]. move=> u v /order_product2_P [us vs [le1 le2]]. rewrite /g LfV // LfV //. move: us vs; rewrite - sy => /setX_P [pu Pu Qu] /setX_P [pv Pv Qv]. move: (Vf_target fy Pu) (Vf_target fy Pv). rewrite ty sr2 //; move/soimP => [[f1 s1 t1] i1]/soimP [[f2 s2 t2] i2]. move: i2 => [_ _ [fw sw tw] iw]; move: (iw _ _ le2) => h'. have h: (gle r'' (Vf (Vf y (P u)) (Q u)) (Vf (Vf y (P v)) (Q u))). move: incy => [_ _ [f3 s3 t3] i3]. by move: (imo_incr or'' (i3 _ _ le1) Qu). order_tac. have sg: source g = (E \times F) by rewrite /g;aw. have sg1: (range (source g) = F) by rewrite sg setX_range. have tg: target g = G by rewrite /g; aw. have axg: inc g (functions (E \times F) G) by apply/functionsP. exists g; first by apply /soimP; split => //; split => //; ue. apply: function_exten. - exact. - exact (proj31 (restriction2_prop (Exercise1_6j ne1 ne2 ig))). - by rewrite /restriction2; aw. - by rewrite /restriction2 ty sr2 //; aw. - move => x xs /=. rewrite restriction2_V //; [ | by apply: Exercise1_6j | ue ]. have xE: inc x E by rewrite /E - sy. rewrite spfa_V //. move: (Vf_target fy xs); rewrite ty sr2 //. move=> /soimP [[fw sw tw] iw]. apply: function_exten => //. - by apply: ( spf_f axg). - by rewrite /second_partial_fun; aw; ue. - by rewrite /second_partial_fun;aw; ue. - rewrite sw; move => i isr /=; rewrite (spf_V axg xE isr) /g LfV//; aw=> //. by apply /setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)