proposition: Lemma Exercise1_4c r r' b c b' c' u: total_order r -> total_order r' -> glt r b c -> glt r' b' c' -> inc u (substrate (order_product2 r r')) -> [\/ least (order_product2 r r') u, greatest (order_product2 r r') u | inc u (ncr_component (order_product2 r r') (J b c'))].
proof: Proof. move:u;move => w [or tor] [or' tor'] ltbc ltbc' us. set r'' := (order_product2 r r'). have or'': order r'' by apply: order_product2_or. move: (ncr_properties or'') => [p1 p2 p3 p4]. have sr'': substrate r'' = (substrate r) \times (substrate r'). rewrite /r'' order_product2_sr //. have bs:inc b (substrate r) by order_tac. have bs':inc b' (substrate r') by order_tac. have cs:inc c (substrate r) by order_tac. have cs':inc c' (substrate r') by order_tac. set C:= (ncr_component r'' (J b c')). have Jas: inc (J b c') (substrate r'') by rewrite sr''; apply /setXp_P. have Jbs: inc (J c b') (substrate r'') by rewrite sr''; apply /setXp_P. have p5: forall x y, not_comp_rel r'' x y -> inc y C -> inc x C. move=> x y h1; rewrite /C -p3 //; move /(class_P p1) => h2. apply /(class_P p1) /(transitivity_e p1 h2 (symmetricity_e p1 (p4 _ _ h1))). have p6: forall x y, not_comp_rel r'' x y -> inc x C -> inc y C. move=> x y h xC;apply: (p5 _ _ _ xC); move: h => [r1 r2 r3]; split => //. case: r3 ; first by move => ->; left. move => h; right => h1; case: h; by case: h1 => h1; [right | left]. have np1: forall u v u' v', glt r u v -> glt r' u' v' -> not_comp_rel r'' (J u v') (J v u'). move => u v u' v' uv uv'; split => //. + rewrite sr''; aw; apply: setXp_i; order_tac. + rewrite sr''; aw; apply: setXp_i; order_tac. + right; case; move / order_product2_P => [_ _] []; aw =>[b1 b2]; order_tac. have JaC: inc (J b c') C by rewrite /C -p3 //; apply /(class_P p1);apply: reflexivity_e => //; ue. have JbC: inc (J c b') C by apply: (p6 _ _ (np1 _ _ _ _ ltbc ltbc') JaC). have p7: forall u, glt r u c -> inc (J u c') C. move=> u u1; by apply: (p5 _ _ (np1 _ _ _ _ u1 ltbc') JbC). have p8: forall u, glt r b u -> inc (J u b') C. move=> u u1; by apply: (p6 _ _ (np1 _ _ _ _ u1 ltbc') JaC). have p9: forall v, glt r' v c' -> inc (J c v) C. move=> v v1; by apply: (p6 _ _ (np1 _ _ _ _ ltbc v1) JaC). have p10: forall v, glt r' b' v -> inc (J b v) C. move=> v v1; by apply: (p5 _ _ (np1 _ _ _ _ ltbc v1) JbC). case:(p_or_not_p(exists2 x, inc x (substrate r'') & ~ gle r'' w x)); last first. move => bad; apply: Or31; split => //; move=> x xsr. case: (p_or_not_p (gle r'' w x)) => // bad1; case: bad; ex_tac. move=> [pt ptr ptc]. case:(p_or_not_p(exists2 x, inc x (substrate r'') & ~ gle r'' x w)); last first. move => bad; apply: Or32; split => //; move=> x xsr. case: (p_or_not_p (gle r'' x w)) => // bad1;case: bad; ex_tac. move=> [gr grr grc]. apply: Or33. have ptd: ~(gle r (P w) (P pt) /\ gle r' (Q w) (Q pt)). move=> [h1 h2]; move: ptc => /order_product2_P; case; split => //; ue. have grd: ~(gle r (P gr) (P w) /\ gle r' (Q gr) (Q w)). move=> [h1 h2]; move: grc => /order_product2_P; case;split => //; ue. move: grr ptr us; rewrite /r'' order_product2_sr//. move=> /setX_P [pgr Pgr Qgr] /setX_P [ppt Ppt Qpt] /setX_P [pw Pw Qw]. move: (tor_prop tor)(tor_prop tor') => to to'. case: (to _ _ Pw bs)=> q1. case: (to' _ _ Qw bs') => q2. case: (to _ _ Pw Ppt)=> q3. case: (to' _ _ Qw Qpt) => q4; first by case: ptd; split => //. have q5: glt r' (Q w) c' by order_tac. have q6: glt r' (Q pt) c' by order_tac. move: (p9 _ q6) => q7. have q8: glt r (P w) c by order_tac. by move: (p5 _ _ (np1 _ _ _ _ q8 q4) q7); rewrite pw. have q5: (glt r (P w) c) by order_tac. have q6: (glt r (P pt) c) by order_tac. move: (p7 _ q6) => q7. have q8: glt r' (Q w) c' by order_tac. by move: (p6 _ _ (np1 _ _ _ _ q3 q8) q7); rewrite pw. move: (p10 _ q2) => q3. have q5: glt r (P w) c by order_tac. move: (p7 _ q5) => q6. case: (equal_or_not (P w) b) => q4. by move: q3; rewrite -q4 pw. have q7: glt r (P w) b by split. move: (p6 _ _ (np1 _ _ _ _ q7 ltbc') q6) => q8. by move: (p5 _ _ (np1 _ _ _ _ q7 q2) q8); rewrite pw. case: (to _ _ cs Pw)=> q1'. case: (to' _ _ cs' Qw) => q2. case: (to _ _ Pgr Pw)=> q3. case: (to' _ _ Qgr Qw) => q4; first by case: grd; split => //. have q5: (glt r' b' (Q w)) by order_tac. have q6: (glt r' b' (Q gr)) by order_tac. move: (p10 _ q6) => q7. have q8: glt r b (P w) by order_tac. by move: (p6 _ _ (np1 _ _ _ _ q8 q4) q7); rewrite pw. have q5: (glt r b (P w)) by order_tac. have q6: (glt r b (P gr)) by order_tac. move: (p8 _ q6) => q7. have q8: glt r' b' (Q w) by order_tac. by move: (p5 _ _ (np1 _ _ _ _ q3 q8) q7); rewrite pw. move: (p9 _ q2) => q3. have q5: glt r b (P w) by order_tac. move: (p8 _ q5) => q6. case: (equal_or_not (P w) c) => q4. by move: q3; rewrite -q4; rewrite pw. have q7: glt r c (P w) by split => //; apply:nesym. move: (p5 _ _ (np1 _ _ _ _ q7 ltbc') q6) => q8. by move: (p6 _ _ (np1 _ _ _ _ q7 q2) q8); rewrite pw. move: (p7 _ q1') (p8 _ q1)=> q1'' q2. case: (to' _ _ Qw bs') => q3; last first. by move:(p5 _ _ (np1 _ _ _ _ q1' q3) JbC); rewrite pw. case: (to' _ _ cs' Qw) => q4; last first. by move:(p6 _ _ (np1 _ _ _ _ q1 q4) JaC); rewrite pw. have q5: (gle r' c' b') by order_tac. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)