proposition: Lemma lucas_injective: injective lucas.
proof: Proof. move => m n; wlog: m n / m < n. move => h;case: (ltngtP m n) => //; first by apply:h. by move => ha hb; symmetry;apply: h. move => lt1;case:(posnP m) => mp sv; last first. by move/andP:(conj mp lt1) => /lucas_smonotone; rewrite sv ltnn. move: lt1 sv; rewrite mp lucas0; case: n => [|[| n]] // _ ha. by move/lucas_monotone: (isT:0 < 2 <= n.+2); rewrite - ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)