proposition: Lemma Zabs_12 : forall z m : Z, (m < Z.abs z)%Z -> {(m < z)%Z} + {(z < - m)%Z}.
proof: Proof. intros [| p| p] m; simpl in |- *; intros H; [ left | left | right; apply Zmin_cancel_Zlt; rewrite Z.opp_involutive ]; assumption. Qed.
imports: Coq(Lia)