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