proposition: Lemma Qabs_opp : forall x, Qabs (-x) == Qabs x.
proof: Proof. intros x. do 2 apply Qabs_case; try (intros; ring); (intros H0 H1; setoid_replace x with 0;[reflexivity|]; apply Qle_antisym);try assumption; rewrite Qle_minus_iff in *; ring_simplify; ring_simplify in H1; assumption. Qed.
imports: QArith Qreduction