proposition: Lemma Exercise1_24f: forall r' X, let r := Qpairi_o in let R := (order_product2 r r') in worder r' -> sub X (substrate R) -> cofinal R X -> anti_directed (induced_order R X) -> False.
proof: Proof. move => r' X r R wor' Xsr cfs anX. have or': order r' by move: wor' => [ok _]. move: Qpairio_osr => [or sr]. have oR: order R by apply: order_product2_or => //. move: (order_product2_sr or or') => sp. set R' := (induced_order R X). rewrite -/R' -/r in sp. set S:= (substrate r) \times (substrate r'). have srR': substrate R' = X by apply: iorder_sr. have oi: order R' by rewrite /R'; apply: (proj1 (iorder_osr oR _)). set Aux:= fun x y => forall z, gle R' x z -> gle R' y z -> False. move: anX => /(Exercise1_23hP oi) [p01 p02]. have p1: forall x y, glt R' x y -> exists2 z : Set, glt R' x z & Aux y z. by rewrite /Aux/R'. have p2: forall x y : Set, inc x (substrate R') -> inc y (substrate R') -> [\/ gle R' x y, gle R' y x, (exists2 x' , gle R' x x' & Aux x' y) | (exists2 y' : Set, gle R' y y'& Aux x y')]. by rewrite /Aux. clear p01 p02. have aux: forall x y,inc x (substrate R') -> inc y (substrate R') -> gle r (P x) (P y) -> ~ (Aux x y). move=> x y xsr ysr pxy aux. rewrite srR' in p2 xsr ysr. have xs1: inc x S by rewrite /S - sp; apply: Xsr. have ys1: inc y S by rewrite /S - sp; apply: Xsr. move: (xs1) (ys1) => /setX_P [px Px Qx] /setX_P [py Py Qy]. move: (worder_total wor') => [_ tor]. case: (tor _ _ Qx Qy) => le2. case: (aux y); first by apply /iorder_gle0P=> //; apply /order_product2_P. order_tac; ue. set t := J (P y) (Q x). have ts: inc t S by rewrite /t;apply /setXp_P;split;fprops. have Rxt: (gle R x t). apply /order_product2_P. by split=> //; split=> //; rewrite /t;aww; order_tac. have Ryt: (gle R y t). apply /order_product2_P. by split=> //; split => //; rewrite /t;aw; trivial;order_tac. have trs: inc t (substrate R) by order_tac. move: cfs => [_ hh]; move: (hh _ trs) => [w wX tw]. case: (aux w); apply /iorder_gle0P => //; order_tac. have aux2: forall x y, inc x (substrate R') -> inc y (substrate R') -> (Aux x y <-> (~ gle r (P x) (P y) /\ ~ gle r (P y) (P x))). move=> x y xsr ysr. case: (p_or_not_p (gle r (P x) (P y))) => r1. move: (aux _ _ xsr ysr r1) => r3. split => // [] [u1 u2] //. case: (p_or_not_p (gle r (P y) (P x))) => r2. move: (aux _ _ ysr xsr r2) => r3. split; last by move=> [u1 u2]. move=> aux3; case: r3 => z z1 z2; case: (aux3 z) => //. split => _; first by split => //. have xs1: inc x S by rewrite /S - sp; apply: Xsr; ue. have ys1: inc y S by rewrite /S - sp; apply: Xsr; ue. move: (xs1) (ys1) => /setX_P [px Px Qx] /setX_P [py Py Qy]. case: (Qpairio_gle4 Px Py); first by done. by done. move => raux z z1 z2. move: (iorder_gle1 z1) (iorder_gle1 z2) => /order_product2_P [_ _ [r3 _]] /order_product2_P [_ _ [r4 _]]. case: (raux _ r3 r4). Abort. End Rat. Module Zermelo. Lemma transfinite_principle_bis r (p:property): worder r -> (forall x, inc x (substrate r) -> (forall y, glt r y x -> p y) -> p x) -> forall x, inc x (substrate r) -> p x. Proof. move => [or wor] hyp x xsr; ex_middle npx. set (X:=Zo (substrate r) (fun x => ~ p x)). have neX: (nonempty X) by exists x; apply: Zo_i. have Xsr: sub X (substrate r) by apply: Zo_S. move:(wor _ Xsr neX)=> [y []]; rewrite iorder_sr // => /Zo_P [ysr npy] yle. case: npy; apply: hyp =>//. move=> t ty; ex_middle npt. have tsr: inc t (substrate r) by order_tac. move: (iorder_gle1 (yle _ (Zo_i tsr npt))) => nty; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)