proposition: Lemma NS_fusc n: natp n -> natp (fusc n).
proof: Proof. move:fusc_pr => [Ha Hb Hc Hd]; move: n. apply: fusc_induction. + by rewrite Ha; fprops. + by rewrite Hb; fprops. + by move => k /Hc ->. + move => k /Hd ->; apply:NS_sum. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)