proposition: Lemma fib_add m n: m != 0 -> fib (m + n) = fib m.-1 * fib n + fib m * fib n.+1.
proof: Proof. elim: m {-2}m (leqnn m) n=> [[] // _ |m IH m1]. rewrite leq_eqVlt; case/orP=> [|Hm]; last first. by apply: IH; rewrite -ltnS. move/eqP->; case: m IH=> [|[|m]] IH n _. - by rewrite mul1n. - by rewrite add2n fibSS addnC !mul1n. - rewrite 2!addSn fibSS -addSn !IH // addnA [fib _ * _ + _ + _]addnAC. by rewrite -addnA -!mulnDl -!fibSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)