proposition: Lemma Qcabs_neg : forall x, x <= 0 -> Qcabs x = - x.
proof: Proof. intros [[[|xn|xn] xd] Hx] H; apply Qc_is_canon; try reflexivity; abstract (compute in H; now elim H). Qed.
imports: Qreduction ClassicalRealizability.Qccomplement