proposition: Lemma Ngcd_fib n m: natp n -> natp m -> Ngcd (Fib n) (Fib m) = Fib (Ngcd n m).
proof: Proof. move => nN mN. move:(cmax_p1 (CS_nat nN)(CS_nat mN)) => [sa sb]. have kN: natp (cmax n m) by apply:Gmax_E. move: nN mN sa sb; move:(cmax n m) kN => k kN; move:k kN n m. apply:Nat_induction. by move=> n m _ _ /cle0 -> /cle0 ->; rewrite Fib0 (Ngcd_n0 NS0) Fib0. move => k kN Hrec n m nN mN le1 le2. wlog lmn: n m nN mN le1 le2 / m <c n. move => H; case: (NleT_ell nN mN); last by apply:H. by move => <-; rewrite (Ngcd_nn (NS_Fib nN)) (Ngcd_nn nN). by rewrite Ngcd_C (Ngcd_C n); apply:H. case: (equal_or_not m \0c) => mz. by rewrite mz Fib0 (Ngcd_n0 nN) (Ngcd_n0 (NS_Fib nN)). move: (cdiff_pr (proj1 lmn)) (NS_diff m nN) ; set r := n -c m => eq1 rN. move: (cpred_pr rN (cdiff_nz lmn)) => [pN pv]. have ha: m <=c k by apply /(cltSleP kN); exact (clt_leT lmn le1). have hb: r <=c k. apply /(cltSleP kN); apply: clt_leT le1. by rewrite - eq1 csumC;apply:(csum_M0lt rN mz). move: (NS_Fib mN) (NS_Fib rN) => fmN frN. move:(NS_Fib (NS_succ mN))(NS_Fib pN) => fsmN fsrN. rewrite - eq1 Ngcd_C (Ngcd_C _ m) (Ngcd_sum mN rN) {1} pv (csum_nS _ pN). rewrite (Fib_add mN pN) csumC - pv (Ngcd_rem fmN (NS_prod fsmN frN) fsrN). rewrite (Ngcd_simp fmN fsmN frN (Ncoprime_Sn_fib mN)). apply:(Hrec _ _ mN rN ha hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)