proposition: Lemma Cminus_diag_uniq : forall z1 z2 : C, z1 - z2 = C0 -> z1 = z2.
proof: Proof. intros z1 z2 H. destruct z1 as (r, r0) ; destruct z2 as (r1, r2) ; rewrite <-Ceq in H ; rewrite <-Ceq ; simpl in *. elim H ; intro H1 ; split ; apply Rminus_diag_uniq ; assumption. Qed.
imports: Ctacfield Cbase Cpow Lia