proposition: Lemma Qcle_abs : forall a, a <= Qcabs a.
proof: Proof. intro a. apply Qcabs_case; auto with *. intro. apply Qle_trans with 0; try assumption. change 0 with (-0). now apply Qcopp_le_compat. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement