proposition: Lemma Qcabs_case (x:Qc) (P : Qc -> Type) : (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P [x].
proof: Proof. intros A B. apply (Qabs_case x (fun x => forall Hx, P {|this:=x;canon:=Hx|})). - intros; case (Qc_decomp x {|canon:=Hx|}); auto. - intros; case (Qc_decomp (-x) {|canon:=Hx|}); auto. Qed.
imports: Qabs Qcanon