proposition: Lemma equation_equiv : forall a b z : C, z = Cplus (Cmult a z) b -> Cmult (Cplus oneC (Copp a)) z = b.
proof: Proof. intros. replace b with (Cplus z (Copp (Cmult a z))). ring. pattern z at 1 in |- *. rewrite H; ring. Qed.