proposition: Lemma lucas_add m n: lucas (n+m).+1 = lucas (n.+1)* fib m.+1 + lucas n * fib m.
proof: Proof. by rewrite (like_fib_shiftE _ _ lucas_like_fib). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)