proposition: Lemma Ncoprime_Sn_fib n: natp n -> Ncoprime (Fib n) (Fib (csucc n)).
proof: Proof. rewrite /Ncoprime;move:n; apply: Nat_induction. by rewrite succ_zero Fib0 Fib1 (Ngcd_0n NS1). move => n nN;rewrite Ngcd_C (Fib_rec nN) csumC (Ngcd_sum); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)