proposition: Lemma fib_sub m n: n <= m -> fib (m - n) = if odd n then fib m.+1 * fib n - fib m * fib n.+1 else fib m * fib n.+1 - fib m.+1 * fib n.
proof: Proof. elim: m n => [|m IH]; first by case. case=> [|n Hn]; first by rewrite muln0 muln1 !subn0. by rewrite subSS IH //=;case:odd; rewrite !fibSS !mulnDr !mulnDl !subnDA !addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)