proposition: Lemma Exercise1_2c1 r1 r2: preorder r1 -> preorder r2 -> weak_order_compatibility (order_product2 r1 r2) (first_proj_eq (substrate r1) (substrate r2)).
proof: Proof. move:(first_proj_equivalence (substrate r1) (substrate r2)) => [q1 q2]. move=> p1 p2; split;first split => //. - by apply: order_product2_preorder. - by rewrite q2 order_product2_sr1. - move=> x y x' /order_product2_P [/setX_P [px px1 qx2] s2 [rp rq]]. move /first_proj_eq_related_P => [_ s3 sp]. move: (s2)(s3) => /setX_P [py py1 qy2] /setX_P [px' px'1 qx'2]. exists (J (P y) (Q x')). by apply /first_proj_eq_related_P; saw; apply /setXp_P. apply /order_product2_P; saw; first by apply /setXp_P. by split => //; [ ue | apply /preorder_reflexivity]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)