proposition: Lemma Qcabs_diff_le_condition x y r: Qcabs (x - y) <= r <-> x - r <= y <= x + r.
proof: Proof. intros. unfold Qcminus. rewrite Qcabs_le_condition. split; intros [Hle₁ Hle₂]; split; rewrite Qcle_minus_iff in *; ring_simplify in Hle₁; ring_simplify in Hle₂; ring_simplify. now replace (y - x + r) with (r - x + y) by ring. now replace (x + r - y) with (x - y + r) by ring. now replace (x - y + r) with (x + r - y) by ring. now replace (r - x + y) with (y - x + r) by ring. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement