proposition: Lemma Sfinite2: C2 <s Nat.
proof: Proof. split. apply: set_le_t =>t /set2_P; case => ->; [apply:NS0 | apply: NS1]. move =>[f [[[ff fi] [_ fs]] sf tf]]. set a := (Vf f C0); set b := Vf f C1. have aN: natp a by rewrite /a /natp; Wtac; rewrite sf;apply: set2_1. have bN: natp b by rewrite /b /natp; Wtac; rewrite sf;apply: set2_2. move:(Nmax_p1 aN bN) =>[cN /(cltSleP cN)/proj2 ha /(cltSleP cN) /proj2 hb]. move:(NS_succ cN); rewrite /natp - tf => /fs [c csf /esym]. by move:csf; rewrite sf; case/set2_P => ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)