proposition: Lemma Qcabs_Q : forall q, Qcabs q == Qabs.Qabs q.
proof: Proof. intro q. apply Qcabs_case; unfold Qcle,Qcopp; repeat rewrite Q2Qc_correct; intro; (now rewrite Qabs.Qabs_pos) || now rewrite Qabs.Qabs_neg. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement