proposition: Lemma NS_Fib_fusc_rec n (v := Fib_fusc_rec n) (a := P v) (b := Q v): natp n -> [/\ (pairp v), natp a & natp b].
proof: Proof. rewrite /a /b/v; move: n {a b v}; apply:Nat_induction. rewrite Fib_fusc_rec0; aw; split; fprops. move => n nN [_ pa pb]; rewrite (Fib_fusc_recS nN) pr1_pair pr2_pair. by split; fprops; apply:NS_succ;apply: NS_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)