proposition: Lemma fusc_induction (p: property): p \0c -> p \1c -> (forall k, natp k -> p k -> p (cdouble k)) -> (forall k, natp k -> p k -> p (csucc k) -> p (csucc (cdouble k))) -> forall n, natp n -> p n.
proof: Proof. move => p0 p1 pe po. have Hr:(forall n, natp n -> (forall k, k<=c n -> p k) -> p (csucc n)). move => n nN Hrec; move:(NS_half (NS_succ nN)) => hN. case:(even_odd_dichot nN). + by move => ->. + by move => [sa sb]; rewrite sa; apply: (pe _ hN); apply: (Hrec _ sb). + by move => [sa sb sc]; rewrite sa; apply: (po _ hN); apply: Hrec. apply: Nat_induction1 => n nN h. case: (equal_or_not n \0c) => nz; first by rewrite nz. move: (cpred_pr nN nz) =>[sa sb]; rewrite sb; apply: (Hr _ sa). by move => k/(cltSleP sa); rewrite - sb; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)