proposition: Lemma Exercise6_31_e: ramifiedc r .
proof: Proof. split; last by apply:Exercise6_31_d. move => x y [lxy /nesym nxy]. move/Exercise6_31_b: lxy => [xE yE stx]. move: (Exercise6_31_c yE) => iby. set a := rep (x -s y). have bb: inc a (x -s y) by apply: rep_i; apply: setC_ne. set z := y -s1 (rep y) +s1 a. have az: inc a z by apply/setU1_P; right. move/setC_P: bb => [ax ay]. move: (stx _ iby) => bx. have bz: ~ (inc (rep y) z). case /setU1_P; first by case/setC1_P. by move => rya; case: ay; rewrite - rya. case: (equal_or_not x z) => xnz; first by case: bz; ue. have zE: inc z inf_subsets. move/Zo_P: xE => [/setP_P xA ix]. move/Zo_P: yE => [/setP_P yA iy]. apply/Zo_P; split. apply/setP_P => t /setU1_P; case; first by move/setC1_P => [/yA]. by move ->; apply/xA. by apply:infinite_setU1; apply: infinite_setC1. exists z; split. - split => //; apply/Exercise6_31_b; split => //. move => t /setU1_P; case; [ by move/setC1_P => [/stx ] | by move -> ]. - by move/Exercise6_31_b =>[_ _ zy]; move: (zy _ az). - by move/Exercise6_31_b =>[_ _ zy]; move: (zy _ iby). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)