proposition: Lemma Qcabs_opp : forall x, Qcabs (-x) = Qcabs x.
proof: Proof. intros x. apply Qcabs_case; intro Hx. rewrite Qcabs_neg. reflexivity. rewrite Qcle_minus_iff in *. now rewrite Qcplus_comm. rewrite Qcle_minus_iff in *. rewrite Qcopp_involutive in *. rewrite Qcplus_0_l in Hx; now rewrite Qcabs_pos. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement