proposition: Lemma Exercise1_22G E: let r := diagonal E in (order_product2 r r = diagonal (E \times E)).
proof: Proof. move=> r. move: (diagonal_osr E) => [or sr]. have h: (forall x y, gle r x y -> x = y). by move=> x y /diagonal_pi_P [_]. set_extens t. move /Zo_P; rewrite sr; move => [ ] /setX_P [pa pb pc] [pd pe]. apply /diagonal_i_P;split => //;move /setX_P: pb => [pf _ _]. move /setX_P: pc => [pg _ _]; apply: pair_exten; fprops. move /diagonal_i_P => [pt] /setX_P [pa pb pc] pd. have pf:inc (P t) (E \times E) by apply /setX_P. have pg: inc (J (P (P t)) (P (Q t))) r by apply /diagonal_pi_P;split => //; ue. have ph: inc (J (Q (P t)) (Q (Q t))) r by apply /diagonal_pi_P;split => //; ue. by apply:Zo_i => //; rewrite sr; apply /setX_P; rewrite -pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)