proposition: Lemma Qcabs_diff_Qcle_condition x y r : [x-y] <= r <-> x - r <= y <= x + r.
proof: Proof. Qc_unfolds; fold (this x) (this y) (this r). case Qred_abs; repeat rewrite Qred_opp. set (a := y) at 1; case (canon y); subst a. set (a := r) at 2; case (canon r); subst a. set (a := Qred r) at 2 3; assert (K := canon (Q2Qc r)); simpl in K; case K; clear K; subst a. set (a := Qred y) at 1; assert (K := canon (Q2Qc y)); simpl in K; case K; clear K; subst a. fold (x - Qred y)%Q (x - Qred r)%Q. destruct (Qabs_diff_Qle_condition x (Qred y) (Qred r)) as [A B]. split. + clear B; rewrite !Qred_le. auto. + clear A; rewrite !Qred_le. auto. Qed.
imports: Qabs Qcanon