proposition: Lemma Cinv_Copp : forall z : C, z <> zeroC -> Cinv (Copp z) = Copp (Cinv z).
proof: Proof. intros. assert (Copp z <> zeroC); auto with geo. assert (Cmult (Copp z) (Copp (Cinv z)) = oneC). 2: apply Cinv_def2; auto. ring_simplify. apply Cinv_def; auto. Qed.