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