proposition: Lemma abs_pos : forall n, 0 < abs n <-> n~=0.
proof: Proof. intros n. rewrite <- abs_0_iff. split; [intros LT| intros NEQ]. - intro EQ. rewrite EQ in LT. now elim (lt_irrefl 0). - assert (LE : 0 <= abs n) by apply abs_nonneg. rewrite lt_eq_cases in LE; destruct LE; auto. elim NEQ; auto with relations. Qed.
imports: ZMulOrder