proposition: Theorem Cmult_distributive : forall z1 z2 z3 : C, Cmult z1 (Cplus z2 z3) = Cplus (Cmult z1 z2) (Cmult z1 z3).
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z1); intros a1 H; elim H; intros b1 H0; try clear H; try exact H0. elim existence_parties_relles_imaginaires with (z := z2); intros a2 H; elim H; intros b2 H1; try clear H; try exact H1. elim existence_parties_relles_imaginaires with (z := z3); intros a3 H; elim H; intros b3 H2; try clear H; try exact H2. rewrite H2; rewrite H1; rewrite H0. repeat rewrite Cmult_algebrique; repeat rewrite Cplus_algebrique; repeat rewrite Cmult_algebrique. replace (a1 * (a2 + a3) + - (b1 * (b2 + b3))) with (a1 * a2 + - (b1 * b2) + (a1 * a3 + - (b1 * b3))); [ idtac | ring ]. replace (b1 * (a2 + a3) + a1 * (b2 + b3)) with (b1 * a2 + a1 * b2 + (b1 * a3 + a1 * b3)); [ auto | ring ]. Qed.