proposition: Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y).
proof: Proof. intros x y. rewrite Qle_minus_iff. setoid_replace (Qabs (x - y) + - (Qabs x - Qabs y)) with ((Qabs (x - y) + Qabs y) + - Qabs x) by ring. rewrite <- Qle_minus_iff. setoid_replace (Qabs x) with (Qabs (x-y+y)). - apply Qabs_triangle. - apply Qabs_wd. ring. Qed.
imports: QArith Qreduction