proposition: Lemma gcd_lucas_fib3 n: (n %%3 !=0) -> coprime (lucas n) (fib n).
proof: Proof. case: n => // n H; rewrite /coprime gcd_lucas_fib1 - (gcdn_modl). by move: (mod3_small n.+1) H; case: (n.+1 %% 3) => [|[ | [| ]]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)