proposition: Lemma abs_0_iff : forall n, abs n == 0 <-> n==0.
proof: Proof. intros n; split. - destruct_max n; auto. now rewrite eq_opp_l, opp_0. - intros EQ; rewrite EQ. rewrite abs_eq; auto using eq_refl, le_refl. Qed.
imports: ZMulOrder