proposition: Lemma Exercise2_3c (r := diagonal C3) (A1:= C0) (A2:= C1): [/\ order r, (ex23_prop r A1 ((substrate r) -s A1)) & (ex23_prop r A2 ((substrate r) -s A2)) ].
proof: Proof. move: (diagonal_osr C3) => []; rewrite -/r => or sr; rewrite sr. have pa: forall A, sub A (substrate r) -> (order_on (induced_order r A) A). by move => A Ai; apply: iorder_osr. have tws: inc C2 (substrate r) by rewrite sr; apply /set3_P; in_TP4. have os: inc C1 (substrate r) by rewrite sr; apply /set3_P; in_TP4. have nc: gle r C1 C2 -> False. move /diagonal_pi_P => [_ bad]; by case: card_12. split; first by exact. have s1: sub A1 (substrate r) by rewrite /A1; fprops. move: (complement_p4 s1) => [ta tb]. move: (pa _ s1) => [tc td]; rewrite - sr; split => //. rewrite {2} /A1 in td. rewrite (empty_substrate_zero td); exact (proj1 set0_wor). have ->: (substrate r -s A1) = substrate r. set_extens t; first by move => /setC_P []. move => ts; apply /setC_P;split => //; case; case. rewrite (iorder_substrate or); move => [y [ysr yl]]. case: (equal_or_not y C1) => y1. by move: (yl _ tws); rewrite y1. by move: (yl _ os) => /diagonal_pi_P [_ bad]. have s1: sub A2 (substrate r). rewrite sr;move => t /set1_P ->; apply /set3_P; in_TP4. move: (complement_p4 s1) => [ta tb]. move: (pa _ s1) => [tc td]; rewrite - sr; split => //. rewrite {2} /A2 in td; exact: (worder_set1 (conj tc td)). have ->: (substrate r -s A2) = doubleton C1 C2. rewrite sr /A2; set_extens t. move /setC_P => []; case /set3_P; first (by move => t1 /set1_P); move => ->; fprops. case /set2_P => ->; apply /setC_P; split; try (apply /set3_P => //;in_TP4); move => /set1_P; fprops. have sd: sub (doubleton C1 C2) (substrate r). by move => t; case /set2_P => ->. move => [y []]; rewrite (iorder_sr or sd) => [te tf]. case: (equal_or_not y C1) => y1. by move: (iorder_gle1 (tf _ (set2_2 C1 C2)));rewrite y1. move: (iorder_gle1 (tf _ (set2_1 C1 C2))). by move /diagonal_pi_P => [_ ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)