proposition: Lemma neq_Zlt (a b : Z) : (a != b) <-> (a < b)%Z \/ (b < a)%Z.
proof: Proof. by split => [/eqP/not_Zeq//|[ab|ba]]; [exact/eqP/ltZ_eqF|exact/eqP/gtZ_eqF]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia