proposition: Lemma gcdn_fib: forall m n, gcdn (fib m) (fib n) = fib (gcdn m n).
proof: Proof. move=> m n; apply: gcdn_def. - by apply: dvdn_fib; exact: dvdn_gcdl. - by apply: dvdn_fib; exact: dvdn_gcdr. move=> d' Hdm Hdn. case: m Hdm=> [|m Hdm]; first by rewrite gcdnE eqxx. have F: 0 < m.+1 by []. case: (egcdnP n F)=> km kn Hg Hl. have->: gcdn m.+1 n = km * m.+1 - kn * n by rewrite Hg addKn. rewrite fib_sub; last by rewrite Hg leq_addr. by case: odd; apply: dvdn_sub; try (by apply: (dvdn_trans Hdn); apply: dvdn_mull; apply: dvdn_fib; apply: dvdn_mull); apply: (dvdn_trans Hdm); apply: dvdn_mulr; apply: dvdn_fib; apply: dvdn_mull. Qed.
imports: mathcomp(all_ssreflect all_algebra)