proposition: Lemma leZ_eqVlt' m n : (m <=? n) = (m == n) || (m <? n).
proof: Proof. apply/idP/idP => [/leZP/leZ_eqVlt[/eqP -> //|/ltZP ->]|/orP[/eqP ->|/ltZP]]. by rewrite orbT. by rewrite leZZ'. by move/ltZP/ltZW'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia