proposition: Lemma up_infinite: infiniteA U inc'.
proof: Proof. move:up_values => [pa pb pc pd [pe pf]]. move:(induction_defined_pr (fun x => g (f x +s1 x)) (g emptyset)). set h:= induction_defined _ _; move => [sh [fh sjh] h0 hr]. exists (g (target h)) => //; split. rewrite pa - h0 /inc' fg; Wtac; rewrite sh; apply:NS0. move => t _; rewrite up_succ /inc' fg; move /sjh => [x xh ->]. by rewrite sh in xh; rewrite - hr //; Wtac; rewrite sh; apply: NS_succ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)