proposition: Lemma existence_solution_equation : forall a b : C, a <> oneC -> exists z : C, z = Cplus (Cmult a z) b.
proof: Proof. intros. cut (Cplus oneC (Copp a) <> zeroC); intros; auto with geo. cut (exists z : C, Cmult (Cplus oneC (Copp a)) z = b); intros. elim H1; intros z H2; try clear H1; try exact H2. exists z. apply equation_equiv2; auto. exists (Cmult (Cinv (Cplus oneC (Copp a))) b). replace (Cmult (Cplus oneC (Copp a)) (Cmult (Cinv (Cplus oneC (Copp a))) b)) with (Cmult (Cmult (Cplus oneC (Copp a)) (Cinv (Cplus oneC (Copp a)))) b); [ idtac | ring ]. rewrite Cinv_def; auto. ring. Qed.