proposition: Lemma leZ_eqVlt m n : (m <= n) <-> (m = n) \/ (m < n).
proof: Proof. split => [|[->|]]. case/Zle_lt_or_eq => ?; by [right|left]. exact: leZZ. exact: ltZW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia