proposition: Lemma Conj_produit : forall z1 z2 : C, Conj (Cmult z1 z2) = Cmult (Conj z1) (Conj z2).
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z1); intros x1 H; elim H; intros y1 H0; try clear H; try exact H0. elim existence_parties_relles_imaginaires with (z := z2); intros x2 H; elim H; intros y2 H1; try clear H; try exact H1. rewrite H1; rewrite H0. rewrite Cmult_algebrique. repeat rewrite Conj_algebrique. rewrite Cmult_algebrique. replace (- y1 * - y2) with (y1 * y2); [ idtac | ring ]. replace (- y1 * x2 + x1 * - y2) with (- (y1 * x2 + x1 * y2)); [ auto | ring ]. Qed.