proposition: Lemma Qabs_triangle : forall x y, Qabs (x+y) <= Qabs x + Qabs y.
proof: Proof. intros [xn xd] [yn yd]. unfold Qplus. unfold Qle. simpl. apply Z.mul_le_mono_nonneg_r;auto with *. change (Zpos yd)%Z with (Z.abs (Zpos yd)). change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. apply Z.abs_triangle. Qed.
imports: QArith Qreduction