proposition: Lemma fib_sub : forall 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 IH]; first by case=> /=. case=> [|n Hn]; first by rewrite muln0 muln1 !subn0. by rewrite -[in odd _]add1n oddD (addTb (odd n)) subSS IH //; case: odd; rewrite !fibSS !mulnDr !mulnDl !subnDA !addKn. Qed.
imports: mathcomp(all_ssreflect all_algebra)