proposition: Lemma Qcabs_triangle_reverse : forall x y, Qcabs x - Qcabs y <= Qcabs (x - y).
proof: Proof. intros x y. rewrite Qcle_minus_iff. setoid_replace (Qcabs (x - y) + - (Qcabs x - Qcabs y)) with ((Qcabs (x - y) + Qcabs y) + - Qcabs x) by ring. rewrite <- Qcle_minus_iff. setoid_replace (Qcabs x) with (Qcabs (x-y+y)). apply Qcabs_triangle. f_equal. ring. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement