proposition: Lemma ltZ_norml x y : `|x| < y <-> (- y < x < y).
proof: Proof. split => [H | [H1 H2] ]. - case: (Z_le_gt_dec x 0) => x0; first by rewrite Zabs_non_eq // in H; lia. rewrite Z.abs_eq // in H; last by lia. by split => //; lia. - case: (Z_le_gt_dec 0 x) => x0; first by rewrite Z.abs_eq. by rewrite Zabs_non_eq; [lia | exact/ltZW/Z.gt_lt]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia