proposition: Lemma lucas_smonotone m n: 0 < m < n -> lucas m < lucas n.
proof: Proof. elim: n=> [|[|n] IH]; first by rewrite andbF. by rewrite ltnS ltnNge; case:leq. rewrite lucasSS andbC; case/andP; rewrite leq_eqVlt; case/orP. by rewrite eqSS; move/eqP=> -> H1m; rewrite -addn1 leq_add // lucas_gt0. by move=> H1m H2m; apply: ltn_addr; apply: IH; rewrite // H2m. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)