proposition: Lemma Qcabs_Qcminus x y: [x-y] = [y-x].
proof: Proof. apply Qc_decomp; Qc_unfolds; fold (this x) (this y) (this (-x)) (this (-y)). set (a := x) at 2; case (canon x); subst a. set (a := y) at 1; case (canon y); subst a. rewrite !Qred_opp; fold (Qred x - Qred y)%Q (Qred y - Qred x)%Q. repeat case Qred_abs; f_equal; apply Qabs_Qminus. Qed.
imports: Qabs Qcanon