proposition: Lemma lucas_monotone m n: 0 < m <= n -> lucas m <= lucas n.
proof: Proof. by rewrite (leq_eqVlt m); case: eqP =>[-> // | _ /lucas_smonotone /ltnW]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)