proposition: Lemma coprime_Sn_fib n: natp n -> coprime (Fib n) (Fib (csucc n)).
proof: Proof. move:n; apply: Nat_induction. rewrite succ_zero Fib0 Fib1; apply: coprime_S; apply:(coprime_1n NS0). by move => n nN /coprime_S Hrec;rewrite (Fib_rec nN); apply:coprime_sum. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)