proposition: Lemma lucas_smonotoneE m n: lucas m < lucas n = [|| (0< m < n), (m==1) && (n== 0)| (m == 0) && (2<= n )].
proof: Proof. case nz: (n==0). rewrite (eqP nz) /= leqn0; case: m => [|[|m]] //. by rewrite ltnNge lucasSS (leq_add (lucas_gt0 m.+1) (lucas_gt0 m)). case mz: (m==0). rewrite (eqP mz) /= lucas0; move: nz; case: n => [|[| n]] // _. by rewrite -[3]/(lucas 2) lucas_monotone. rewrite andbF /= orbF; case: (ltnP m n) => h. by rewrite lucas_smonotone ?h lt0n mz. by rewrite ltnNge lucas_monotone lt0n ?mz // nz h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)