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