proposition: Lemma Exercise1_6m: nonempty E -> nonempty F -> order_isomorphism (second_partial_map2 r r' r'') (increasing_mappings_order (order_product2 r r') r'') (increasing_mappings_order r (increasing_mappings_order r' r'')).
proof: Proof. move=> ne1 ne2. move: (Exercise1_6l ne1 ne2). set f := (second_partial_map2 r r' r''); move=> [bf sf tf]. have ta:= (Exercise1_6k ne1 ne2). have [o2 sr2]:= (imo_osr r' or''). have o3:order (order_product2 r r') by apply: order_product2_or. have [o2' sr2']:= (imo_osr (order_product2 r r') or''). have [o2'' sr2''] := (imo_osr r o2). split => //; first by rewrite sr2' sr2''. move=> x y xsf ysf. have sop:= (order_product2_sr or or'). move: (xsf) (ysf); rewrite sf; move /soimP => [[fx sx tx] ix]. move /soimP => [[fy sy ty] iy]. rewrite sop in sx sy. have axx: inc x (functions (E \times F) G) by apply/functionsP. have axy: inc y (functions (E \times F) G) by apply/functionsP. have ff: function f by fct_tac. have u1p: inc (Vf (second_partial_map2 r r' r'') x) (target (second_partial_map2 r r' r'')) by Wtac. have u2p: inc (Vf (second_partial_map2 r r' r'') y) (target (second_partial_map2 r r' r'')) by Wtac. move: (Exercise1_6j ne1 ne2 ix)(Exercise1_6j ne1 ne2 iy) => ta1 ta2. split. move /(imo_gleP _ or'') => [_ _ incx]. apply /(imo_gleP _ o2);rewrite -tf; split => //. rewrite /f LfV //; last (by ue);rewrite LfV //; last (by ue). split => //; rewrite ? sr2. split => //;rewrite /restriction2; aw; trivial. by apply: (proj31 (restriction2_prop ta1)). split => //;rewrite /restriction2; aw; trivial. by apply: (proj31 (restriction2_prop ta2)). move => i isr; rewrite restriction2_V //restriction2_V //. rewrite spfa_V // spfa_V //; apply /(imo_gleP _ or''). have in1:= (Exercise1_6i ne1 ne2 ix isr). have in2 :=(Exercise1_6i ne1 ne2 iy isr). move: (in1)(in2) => [_ _ [f1 s1 s'1] i1] [_ _ [f2 s2 s'2] i2]. split => //; try apply /soimP;split => //. move=> j jsr'. rewrite (spf_V axx isr jsr') (spf_V axy isr jsr'). apply: (proj33 incx); rewrite sop; fprops. move => h. apply /(imo_gleP _ or''); rewrite - sf; split => //; hnf; rewrite sop. split => // i /setX_P [pi Pi Qi]. rewrite - pi; move:(imo_incr o2 h Pi). rewrite /f LfV //; last (by ue);rewrite LfV //; last (by ue). rewrite restriction2_V // restriction2_V // spfa_V // spfa_V //. move => h1; move: (imo_incr or'' h1 Qi). by rewrite (spf_V axx Pi Qi) (spf_V axy Pi Qi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)