proposition: Lemma cc_minus_abs : forall x y : CC, AbsCC (x[-]y) [=] AbsCC (y[-]x).
proof: Proof. intros. apply eq_transitive_unfolded with (AbsCC [--] (y[-]x)). apply AbsCC_wd. rational. apply cc_inv_abs. Qed.
imports: CoRN.complex.CComplex