proposition: Lemma Fib_fusc_val n: natp n -> (fusc (Fib_fusc n)) = Fib n.
proof: Proof. move: n. suff: forall n, natp n -> (fusc (Fib_fusc n)) = Fib n /\ (fusc (Fib_fusc (csucc n))) = Fib (csucc n). by move => H n nN; move:(H _ nN) => []. apply: Nat_induction. rewrite /Fib_fusc Fib_fusc_rec0 Fib_fusc_rec1; aw. by rewrite succ_zero Fib0 Fib1 fusc0 fusc1. by move => n nN [sa sb]; rewrite(Fib_fusc_rec_frec nN) sb sa (Fib_rec nN) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)