proposition: Lemma Cadd_neq_compat_l : forall z z' : C, z' <> C0 -> z + z' <> z.
proof: Proof. intros z z' z'_neq Hf ; apply z'_neq. assert (H := Cadd_eq_compat_l (- z) _ _ Hf). rewrite <- Cadd_assoc, Cadd_opp_l, Cadd_0_l in H ; assumption. Qed.
imports: Ctacfield Cbase Cpow Lia