proposition: Lemma Qcabs_case : forall (x:Qc) (P : Qc -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qcabs x).
proof: Proof. intros x P H1 H2. unfold Qcabs. destruct x as [[[|xn|xn] xd] Hx]; simpl; (apply H1 || apply H2; abstract (compute; discriminate)). Qed.
imports: Qreduction ClassicalRealizability.Qccomplement