proposition: Lemma ltZ_neqAle' m n : (m <? n) = (m != n) && (m <=? n).
proof: Proof. apply/idP/idP => [/ltZP mn|]. by apply/andP; split; [apply/eqP; lia | exact/ltZW'/ltZP]. by case/andP => /eqP H1 /leZP H2; apply/ltZP; lia. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia