proposition: Lemma Qcabs_Qcle_condition x y : [x] <= y <-> -y <= x <= y.
proof: Proof. Qc_unfolds; fold (this x) (this y). destruct (Qabs_Qle_condition x y) as [A B]. split; intros H. + destruct (A H) as [X Y]; split; auto. now case (canon x); apply Qred_le. + destruct H as [X Y]; apply B; split; auto. now case (canon y); case Qred_opp. Qed.
imports: Qabs Qcanon