proposition: Lemma ltZ_neqAle m n : (m < n) <-> (m <> n) /\ (m <= n).
proof: Proof. split => [mn|[H]]; last by rewrite leZ_eqVlt => -[|]. by split; [exact/nesym/gtZ_eqF | exact/ltZW]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia