proposition: Lemma Qabs_case : forall (x:Q) (P : Q -> Type), (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P (Qabs x).
proof: Proof. intros x P H1 H2. destruct x as [[|xn|xn] xd]; [apply H1|apply H1|apply H2]; abstract (compute; discriminate). Defined.
imports: QArith Qreduction