proposition: Lemma Cmult_associative : forall z1 z2 z3 : C, Cmult z1 (Cmult z2 z3) = Cmult (Cmult z1 z2) z3.
proof: Proof. intros. elim (classic (z1 = zeroC)); intros. rewrite H. repeat rewrite Cmult_zeroC_z; auto. elim (classic (z2 = zeroC)); intros. rewrite H0. repeat rewrite Cmult_zeroC_z; repeat rewrite Cmult_z_zeroC; repeat rewrite Cmult_zeroC_z; auto. elim (classic (z3 = zeroC)); intros. rewrite H1. repeat rewrite Cmult_z_zeroC; auto. apply egalite_forme_polaire. apply nonzero_produit; auto with geo. apply nonzero_produit; auto with geo. repeat rewrite Cmult_module; ring. repeat rewrite Cmult_argument; auto with geo. elim existence_argument with (z := z1); [ intros a H2; try clear existence_argument; try exact H2 | auto with geo ]. elim existence_argument with (z := z2); [ intros a0 H3; try clear existence_argument; try exact H3 | auto with geo ]. elim existence_argument with (z := z3); [ intros a1 H4; try clear existence_argument; try exact H4 | auto with geo ]. rewrite H2; rewrite H3; rewrite H4. repeat rewrite <- add_mes_compatible. replace (a + (a0 + a1)) with (a + a0 + a1); [ auto | ring ]. Qed.