proposition: Lemma Qcabs_minus x y: Qcabs (x - y) = Qcabs (y - x).
proof: Proof. setoid_rewrite <- Qcopp_involutive at 2. rewrite Qcabs_opp. unfold Qcminus. rewrite Qcopp_distr_plus. rewrite Qcopp_involutive. now rewrite Qcplus_comm. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement