proposition: Lemma Fib_fusc_recS n (v := Fib_fusc_rec n) (a := P v) (b := Q v) : natp n -> Fib_fusc_rec (csucc n) = J (csucc (cdouble b)) (a +c b).
proof: Proof. apply:induction_terms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)