proposition: Lemma Qabs_diff_Qle x y r: (Qabs (x - y) <= r) <-> (x - r <= y <= x + r).
proof: Proof. Proof with try ring. intros. rewrite Qabs_Qle. rewrite <- (Qplus_le_r (r + y) (-r) (x- y)). rewrite <- (Qplus_le_r (y - r) (x-y) r). setoid_replace (r + y + -r) with y... setoid_replace (r + y + (x - y)) with (x + r)... setoid_replace (y - r + (x - y)) with (x - r)... setoid_replace (y - r + r) with y... intuition. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List