proposition: Lemma fusc_nz n: natp n -> n <> \0c -> (fusc n) <> \0c.
proof: Proof. move:fusc_pr => [Ha Hb Hc Hd]; move: n. apply: fusc_induction. + by case. + by rewrite Hb. + move => k /Hc -> pa pb. by apply: pa => kz; case: pb; rewrite kz cdouble0. + move => k /Hd -> _ pa _ /csum_nz [_]; apply/pa; apply:succ_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)