proposition: Lemma lucas_monotone2 n p: p <= n -> lucas (n - p) <= lucas (n + p).
proof: Proof. move/subnK => {2} <-; rewrite -addnA addnn lucas_monotoneE. case pz:(p==0); first by rewrite (eqP pz) addn0 eqxx. have p2: 2 <= p.*2 by rewrite (leq_double 1 p) lt0n pz. rewrite (ltn_paddr _ (ltnW p2)) (leq_trans p2 (leq_addl _ p.*2)) lt0n !andbT. by case np: (n-p==0); rewrite ? orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)