proposition: Lemma unicite_solution_equation : forall a b z z' : C, a <> oneC -> z = Cplus (Cmult a z) b -> z' = Cplus (Cmult a z') b -> z = z'.
proof: Proof. intros. cut (Cplus z (Copp z') = zeroC); intros. replace z with (Cplus (Cplus z (Copp z')) z'); [ idtac | ring ]. rewrite H2; ring. apply Cintegre with (z := Cplus oneC (Copp a)); auto with geo. cut (Cmult (Cplus oneC (Copp a)) z = b); intros. 2: apply equation_equiv; auto. cut (Cmult (Cplus oneC (Copp a)) z' = b); intros. 2: apply equation_equiv; auto. replace zeroC with (Cplus b (Copp b)); [ idtac | ring ]. pattern b at 1 in |- *. rewrite <- H2. rewrite <- H3; ring. Qed.