proposition: Lemma Qcabs_neg x : x <= 0 -> [x] = - x.
proof: Proof. intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x). set (K := canon [x]); simpl in K; case K; clear K. now apply Qred_complete; apply Qabs_neg. Qed.
imports: Qabs Qcanon