proposition: Lemma Exercise6_31_d: ~ (exists x : Set, maximal r x).
proof: Proof. move => [x [xsr xmax]]. move: Exercise6_31_a =>[or sr]. rewrite sr in xsr; move/Zo_P: (xsr) => [/setP_P xA ix]. set y := (x -s1 (rep x)). have id : infinite_set y by apply:infinite_setC1. have syx: sub y x by move => t /setC1_P []. have dZ: inc y inf_subsets. apply:Zo_i => //; apply/setP_P; apply: (sub_trans syx xA). have /xmax eq: gle r x y by apply/Exercise6_31_b. by move: (Exercise6_31_c xsr); rewrite - {2} eq => /setC1_P [_]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)