proposition: Lemma fibt_aux (n k: nat) : fibt n (fib k.+1) (fib k) = fib (n + k).+1.
proof: Proof. elim: n k => [ | n Ih] k. by []. rewrite -[fibt n.+1 _ _]/(fibt n (fib k.+2) (fib k.+1)). rewrite Ih. by rewrite addnS addSn. Qed.
imports: Coq(Extraction ZArith Lia) mathcomp(all_ssreflect all_algebra)