proposition: Lemma Cmult_commutative : forall z z' : C, Cmult z z' = Cmult z' z.
proof: Proof. intros. elim (classic (z = zeroC)); intros. rewrite H; rewrite Cmult_zeroC_z; rewrite Cmult_z_zeroC; auto. elim (classic (z' = zeroC)); intros. rewrite H0; rewrite Cmult_zeroC_z; rewrite Cmult_z_zeroC; auto. elim existence_forme_polaire with (z := z); [ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1 existence_forme_polaire; try exact H3 | auto with geo ]. elim existence_forme_polaire with (z := z'); [ intros r' H5; elim H5; intros a' H6; elim H6; intros H7 H8; try clear H6 H5 existence_forme_polaire; try exact H7 | auto with geo ]. rewrite (Cmult_z_z' (z:=z) (z':=z') (r:=r) (a:=a) (r':=r') (a':=a')); auto with geo. rewrite (Cmult_z_z' (z:=z') (z':=z) (r:=r') (a:=a') (r':=r) (a':=a)); auto with geo. replace (r * r') with (r' * r); [ idtac | ring ]. replace (a + a') with (a' + a); [ auto | ring ]. Qed.