proposition: Lemma fibtP (n : nat) : fibt n 1 0 = fib n.
proof: Proof. case: n => [ | p]. by []. rewrite [LHS]/= add0n -[in RHS](addn0 p). by rewrite -fibt_aux. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)