proposition: Lemma Qcabs_opp x : [(-x)] = [x].
proof: Proof. apply Qc_decomp; Qc_unfolds; fold (this x). set (K := canon [x]); simpl in K; case K; clear K. case Qred_abs; apply Qred_complete; apply Qabs_opp. Qed.
imports: Qabs Qcanon