proposition: Lemma Exercise1_2c2 r1 r2 (p :=first_proj_eq (substrate r1) (substrate r2)) : preorder r1 -> preorder r2 -> ne_substrate r1 -> (Ex1_2_strong_l (order_product2 r1 r2) p \/ Ex1_2_strong_r (order_product2 r1 r2) p) -> r2 = coarse (substrate r2).
proof: Proof. move=> p1 p2 [x xr1] cp. have p3: (preorder (order_product2 r1 r2)) by apply: order_product2_preorder. set_extens t => ts. apply /setX_P;split; first exact:(proj31 p2 _ ts); substr_tac. move/setX_P: ts => [pt ps qs]. set X := ((substrate r1) \times (substrate r2)). have x1p:inc (J x (P t)) X by rewrite /X; fprops. have x2p:inc (J x (Q t)) X by rewrite /X; fprops. have rp: forall s, inc s X -> gle (order_product2 r1 r2) s s. by move => s H; apply/(preorder_reflexivity _ p3);rewrite order_product2_sr1. move: (rp _ x1p) (rp _ x2p) => r11 r22. have s12: (related p (J x (P t)) (J x (Q t))). apply /first_proj_eq_related_P; saw. have s21: (related p (J x (Q t)) (J x (P t))). apply /first_proj_eq_related_P; saw. rewrite - pt; case: cp => cp. by move: (cp _ _ _ r22 s21) => /order_product2_P [_ _ [_] ]; aw. by move: (cp _ _ _ r11 s12) => /order_product2_P [_ _ [_] ]; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)