proposition: Lemma Cinv_Cmult : forall z z' : C, z <> zeroC -> z' <> zeroC -> Cinv (Cmult z z') = Cmult (Cinv z) (Cinv z').
proof: Proof. intros. assert (Cmult z z' <> zeroC); [ auto with geo | idtac ]. assert (Cmult (Cmult z z') (Cmult (Cinv z) (Cinv z')) = oneC). replace (Cmult (Cmult z z') (Cmult (Cinv z) (Cinv z'))) with (Cmult (Cmult z (Cinv z)) (Cmult z' (Cinv z'))); [ idtac | ring ]. rewrite Cinv_def; auto. rewrite Cinv_def; auto. ring. apply Cinv_def2; auto. Qed.