proposition: Lemma Qabs_neg : forall x, x <= 0 -> Qabs x == - x.
proof: Proof. intros x H. apply Qabs_case. - intros H0. setoid_replace x with 0. + reflexivity. + apply Qle_antisym; assumption. - reflexivity. Qed.
imports: QArith Qreduction