proposition: Lemma Exercise1_22H: exists r, let r' := order_product2 r r in order r /\ (exists2 t, open_o r' t & forall a b, t <> a \times b).
proof: Proof. move: (Exercise1_22G C2). set r := diagonal C2 ; move => /= ta. move: (diagonal_osr C2) => [or sr]. exists r; split => //. exists ((C2 \times C2) -s1 (J C0 C0)). by rewrite ta; apply Exercise1_22F; move => t /setC1_P []. move => a b eq. have pa: inc (J C0 C1) (a \times b). rewrite - eq; apply /setC1_P; split; first by apply:setXp_i; fprops. move =>ba; move: (pr2_def ba); fprops. have pb: inc (J C1 C0) (a \times b). rewrite - eq; apply /setC1_P; split; first by apply:setXp_i; fprops. move =>ba; move: (pr1_def ba); fprops. move: pa pb => /setXp_P [pa _] /setXp_P [_ pb]. have : inc (J C0 C0) (a \times b) by apply:setXp_i; fprops. by rewrite -eq => /setC1_P [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)