proposition: Lemma Exercise6_31_g: ~ anti_directed r.
proof: Proof. move => h. move :Exercise6_31_a =>[or sr]. move/ (Exercise1_23hP or): h =>[qa _]. have aE: inc A inf_subsets by apply: Zo_i => //; apply: setP_Ti. set X := A -s1 (rep A). have sXA: sub X A by move => t /setC1_P; case. have xE: inc X inf_subsets. by apply: Zo_i; [by apply/setP_P | apply: infinite_setC1]. move: (Exercise6_31_c aE) => raa. have nAX: A <> X. by move => h; move: raa; rewrite{2} h => /setC1_P [_]. have lxA: glt r A X. by split => //; apply/Exercise6_31_b. move: (qa _ _ lxA) =>[z laz]. move/(Exercise6_31_b): (proj1 laz) => /proj32 zE. move/(Exercise6_31_f xE zE) => ifin. move/Zo_P: (zE) => [/setP_P szA iz]. apply:(finite_not_infinite_set ifin). move: (infinite_setC1 (rep A) iz). have <- //: (X \cap z) = z -s1 (rep A). set_extens t. by move => /setI2_P [/setC1_P [ua ub] uc]; apply/setC1_P. move => /setC1_P [tz tra]; apply/setI2_P; split => //. by apply/setC1_P; split => //; apply: szA. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)