proposition: Lemma abs_le : forall a b, abs a <= b <-> -b <= a <= b.
proof: Proof. intros a b. destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ. - split; try split; try destruct 1; try order. apply le_trans with 0; trivial. apply opp_nonpos_nonneg; order. - rewrite opp_le_mono, opp_involutive. split; try split; try destruct 1; try order. apply le_trans with 0. + order. + apply opp_nonpos_nonneg; order. Qed.
imports: ZMulOrder