proposition: Lemma gcd_lucas_fib1 n: gcdn (lucas n.+1) (fib n.+1) = fib (gcdn n.+1 3).
proof: Proof. have h: coprime (fib n.+1) (fib n) by rewrite coprime_sym coprimeSn_fib. by rewrite gcdnC lucasS gcdnDl - muln2 Gauss_gcdr //(gcd_fib _ 3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)