proposition: Lemma Qcabs_le_condition x y: Qcabs x <= y <-> -y <= x <= y.
proof: Proof. split. split. rewrite <- (Qcopp_involutive x). apply Qcopp_le_compat. apply Qcle_trans with (Qcabs (-x)). now apply Qcle_abs. now rewrite Qcabs_opp. transitivity (Qcabs x); auto using Qcle_abs. intros [? ?]. unfold Qcle. apply Qcabs_case; trivial. intros. rewrite <- (Qcopp_involutive y). now apply Qcopp_le_compat. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement