proposition: Lemma Copp_neq_0_compat : forall z : C, z <> C0 -> - z <> C0.
proof: Proof. intros z H Habs. apply Copp_eq_0_compat in Habs. rewrite Copp_involutive in Habs. apply H ; assumption. Qed.
imports: Ctacfield Cbase Cpow Lia