proposition: Lemma gcd_lucas_fib2 n: (n %%3 ==0) -> gcdn (lucas n) (fib n) = 2.
proof: Proof. by case: n => // n H; rewrite gcd_lucas_fib1 - (gcdn_modl) (eqP H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)