proposition: Lemma Qcabs_pos x : 0 <= x -> [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. set (a := x) at 1; case (canon x); subst a; apply Qred_complete. now apply Qabs_pos. Qed.
imports: Qabs Qcanon