proposition: Lemma infinite_depth_prop x (f := rept_union x): (forall n, natp n -> (finite_set (f n) /\ nonempty (f n))) -> ~ (well_founded_set x).
proof: Proof. rewrite /f. pose H x :=(forall n, inc n Nat -> finite_set (rept_union x n) /\ nonempty (rept_union x n)). rewrite -/(H x) => Hx wfx. have aux: (forall x, H x -> exists2 y, inc y x & H y). move => z hz; ex_middle bad. move: (proj1 (rept_union_pr z)) => h0. case: (emptyset_dichot z) => znz. by move: (proj2 (hz _ NS0)); rewrite h0 znz; move => [t /in_set0]. pose Ha x := (forall n, inc n Nat -> finite_set (rept_union x n)). have hay: forall y, inc y z -> Ha y. move => y yz n nN; move: (proj1 (hz _ (NS_succ nN))) => tu. by move: (rept_union_inc yz nN) => /sub_finite_set; apply. have hby: forall y, inc y z -> exists2 n, inc n Nat & (rept_union y n) = emptyset. move => y yz; ex_middle bad2; case: bad; ex_tac. move => n nN; split; first by apply: (hay _ yz _ nN). case: (emptyset_dichot (rept_union y n)) => // h; case: bad2; ex_tac. pose q y n := inc n Nat /\ (rept_union y n) = emptyset. pose tn y:= choose (q y). have tnp: forall y, inc y z -> q y (tn y). by move => y /hby [n nb etc]; apply: choose_pr; exists n. have tmp: forall y m, inc y z -> inc m Nat -> (tn y) <=c m -> rept_union y m = emptyset. move => y m yz mN le; rewrite - (cdiff_pr le); move: (NS_diff (tn y) mN). move: (tnp _ yz) => [sa sb]. move: (m -c tn y); apply : Nat_induction; first by rewrite csum0r; fprops. move => n nN;rewrite (csum_nS _ nN). rewrite (proj2(rept_union_pr y) _ (NS_sum sa nN)) => ->; exact setU_0. have [n nN pn]: exists2 n, inc n Nat & forall y, inc y z -> (tn y) <=c n. set s := fun_image z tn. have p1: sub s Nat by move => y /funI_P [t /tnp [aa _] ->]. have p2: finite_set s. by apply finite_fun_image; move: (proj1 (hz _ NS0)); rewrite h0. have p3: nonempty s by apply: funI_setne. move: (finite_subset_Nat p1 p2 p3) => [n ns etc]. exists n; first by apply: p1. move => y yz; apply: etc; apply /funI_P; ex_tac. move: (proj2 (hz _ (NS_succ nN))) => [s sp]. move: (rept_union_inc2 nN sp) => [y yz]. by rewrite (tmp _ _ yz nN (pn _ yz)) => /in_set0. pose p x y:= (inc y x /\ H y); pose nf x := choose (p x). move: (induction_defined_pr nf x); set g := induction_defined nf x. move => [pa pb pc pd]. have pe: (forall n, inc n Nat -> inc (Vf g (csucc n)) (Vf g n)). have px: forall x, H x -> p x (nf x). by move => z /aux [y yz hy]; apply: (choose_pr); exists y. have py: forall n, inc n Nat ->p (Vf g n) (Vf g (csucc n)). apply: Nat_induction; first by rewrite (pd _ NS0) pc; apply: px. by move => n nN [_ h]; rewrite (pd _ (NS_succ nN)); apply: px. by move => n /py []. by case: (wfx g (proj1 pb) pa pe); rewrite - pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)