proposition: Lemma Exercise1_6g: order_isomorphism (two_projections_increasing r r' r'') (increasing_mappings_order r (order_product2 r' r'')) (order_product2 (increasing_mappings_order r r') (increasing_mappings_order r r'')).
proof: Proof. have orp: order (order_product2 r' r'') by apply: order_product2_or. move: (imo_osr r or') (imo_osr r or'') => [o1 sr1] [o2 sr2]. move: (imo_osr r orp) => [o3 sr3]. split => //; first by apply: order_product2_or => //. split => //. + by apply: Exercise1_6f. + by rewrite /two_projections_increasing /restriction2 sr3; aw. + by rewrite order_product2_sr // sr1 sr2 corresp_t. hnf;rewrite corresp_s => x y xsi ysi. move: (xsi) (ysi)=> /(soimP) [[fx sx tx] ix] /(soimP) [[fy sy ty] iy]. move: (@two_projections_ax E F G) => t1. move: (Exercise1_6e) => ra. rewrite restriction2_V // restriction2_V //. rewrite order_product2_sr // in tx ty. move: (two_projections_aux fx sx tx) => [p1 p2 p3 p4 [p5 p6]]. move: (two_projections_aux fy sy ty) => [q1 q2 q3 q4 [q5 q6]]. move: ra => []; rewrite lf_source => ftp sstp sttp saux. move: (sstp _ xsi) (sstp _ ysi) => xsi' ysi'. rewrite /two_projections LfV // LfV //. move: (Exercise1_6d ix) (Exercise1_6d iy). move: p3 p4 p5 p6 q3 q4 q5 q6. set (f1 := first_projection x E F). set (f2 := secnd_projection x E G). set (f3 := first_projection y E F). set (f4 := secnd_projection y E G). move=> p3 p4 p5 p6 q3 q4 q5 q6 [if1 if2][if3 if4]. split; last first. move /order_product2_P => [_ _[] ];rewrite ! pr1_pair ! pr2_pair. move /(imo_gleP r or') => [Sf1 Sf3 if13]/(imo_gleP r or'') [Sf2 Sf4 if24]. apply /(imo_gleP r orp);rewrite order_product2_sr //;split => //; split => //. move=> i isr; apply /order_product2_P; rewrite - {1} tx -ty. rewrite -(q5 _ isr) - (q6 _ isr) -(p5 _ isr) - (p6 _ isr). move: if13 if24 => [_ _ s1] [_ _ s2]. split; [ Wtac | Wtac | split; fprops]. move => xx; move: (imo_incr orp xx) => h3. move /(imo_gleP r orp):xx => [h1 h2 _]. apply /order_product2_P; rewrite sr1 sr2. have sf1: (source f1 = E) by rewrite /f1 /first_projection; aw. have sf2: (source f2 = E) by rewrite /f2 /secnd_projection; aw. have sf3: (source f3 = E) by rewrite /f3 /first_projection; aw. have sf4: (source f4 = E) by rewrite /f4 /secnd_projection; aw. have tf1: (target f1 = F) by rewrite /f1 /first_projection; aw. have tf2: (target f2 = G) by rewrite /f2 /secnd_projection; aw. have tf3: (target f3 = F) by rewrite /f3 /first_projection; aw. have tf4: (target f4 = G) by rewrite /f4 /secnd_projection; aw. have Sf1: (inc f1 (increasing_mappings r r')) by apply /soimP. have Sf2: (inc f2 (increasing_mappings r r'')) by apply /soimP. have Sf3: (inc f3 (increasing_mappings r r')) by apply /soimP. have Sf4: (inc f4 (increasing_mappings r r'')) by apply /soimP. split; [by apply setXp_i | by apply setXp_i | aw; split]. apply /(imo_gleP r or');split => //; split => //. move=> i isr; rewrite (p5 _ isr) (q5 _ isr). by move: (h3 _ isr) => /order_product2_P [_ _ []]. apply /(imo_gleP r or'');split => //; split => //. move=> i isr; rewrite (p6 _ isr) (q6 _ isr). by move: (h3 _ isr) => /order_product2_P [_ _ []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)