proposition: Lemma Exercise1_22I: exists r, let r' := order_product2 r r in let R := reg_open_order r in order r /\ not(reg_open_order r' \Is order_product2 R R).
proof: Proof. set E := singleton \0c. move: (Exercise1_22G E) => /=. move: (diagonal_osr E) => []; set r := diagonal E => od sr h. exists r; split => //; move => [f [_ _ [bf sf tf] _]]. move: (proj1 (Exercise1_22y od)) => oR. move: sf tf. rewrite order_product2_sr // /reg_open_order (proj2 (sub_osr _)) => sf tf. have sr0: inc \0c (substrate r) by rewrite sr /E; fprops. have nef: nonempty (substrate r) by exists \0c. have rr: right_directed r. split => // x y; rewrite sr => /set1_P-> /set1_P ->; exists \0c;split => //. by move =>t /set1_P ->; order_tac. set r' := (order_product2 r r). have sr': substrate r' = E \times E by rewrite order_product2_sr // sr. have sr0': inc (J \0c \0c) (substrate r') by rewrite sr' ; apply /setXp_P;split => //; ue. have see: forall x, inc x (E \times E) -> x = J \0c \0c. move => x => /setX_P [ta] /set1_P tb / set1_P tc. by rewrite - ta tb tc. have nef': nonempty (substrate r') by exists (J \0c \0c). have or': order r' by apply: order_product2_or. have rr': right_directed r'. split => // x y; rewrite sr' => xsr ysr; rewrite (see _ xsr) (see _ ysr). exists (J \0c \0c); split => //. by move =>t ; case /set2_P => ->; order_tac. move: (proj2 (Exercise1_22qP od) (conj nef rr)) => [a [b [ab eab]]]. move: (cardinal_set2 ab); rewrite -eab => c1. move: (f_equal cardinal tf); rewrite - cprod2_pr1. rewrite (proj2 (sub_osr _)) - cprod2cl - cprod2cr c1. move: (proj2 (Exercise1_22qP or') (conj nef' rr')) => [a' [b' [ab' eab']]]. move: (cardinal_set2 ab'); rewrite -eab';rewrite - sf. have->: (cardinal (source f) = cardinal (target f)) by apply /card_eqP; exists f;split => //. move => ->;rewrite cprod_22; exact:(proj2 clt_24). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)