proposition: Lemma Qcabs_inv : forall a, Qcabs (/ a) = / Qcabs a.
proof: Proof. intro a. apply (Qcabs_case a); intro Ha. apply Qcabs_pos. now rewrite Qcinv_nonneg. rewrite Qcinv_opp_comm. apply Qcabs_neg. now rewrite Qcinv_nonpos. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement