proposition: Lemma leZ_nat n m : (n <= m)%nat = (n%:Z <=? m%:Z).
proof: Proof. case/boolP : (n <= m)%nat => H; first by apply/esym/leZP/Nat2Z.inj_le/leP. by apply/esym/negbTE; by apply: contra H => /leZP/Nat2Z.inj_le/leP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia