proposition: Lemma gcd_fib n m: gcdn (fib n) (fib m) = fib (gcdn n m).
proof: Proof. move: (leq_maxl n m) (leq_maxr n m);move:(maxn _ _)=> k. elim: k n m; [ by case; [case |] | move => max Hrec n m le1 le2 ]. wlog lmn: n m le1 le2 / n < m. move => H; case: (ltngtP n m) => aux; first by apply: H. by rewrite gcdnC (gcdnC n); apply: H. by rewrite aux !gcdnn. case (posnP n); first by move => ->; rewrite! gcd0n. move:(subnK (ltnW lmn));set r := m - n => eq1 np. move:(lmn); rewrite - subn_gt0 lt0n => rnz. move:(ltn_sub2l (ltn_trans np lmn) np); rewrite subn0 => ha. rewrite -eq1 gcdnDr fib_add // gcdnMDl (Gauss_gcdl _ (coprimeSn_fib n)). by rewrite Hrec // - ltnS; apply: (leq_trans _ le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)