proposition: Theorem Cmult_algebrique : forall x1 y1 x2 y2 : R, Cmult (cons_cart x1 y1) (cons_cart x2 y2) = cons_cart (x1 * x2 + - (y1 * y2)) (y1 * x2 + x1 * y2).
proof: Proof. intros. elim (classic (cons_cart x1 y1 = zeroC)); intros. elim algebrique_zeroC with (a := x1) (b := y1); [ intros; try exact H1 | auto ]. rewrite H1; rewrite H0. replace (0 * x2 + - (0 * y2)) with 0; [ idtac | ring ]. replace (0 * x2 + 0 * y2) with 0; [ idtac | ring ]. repeat rewrite Cmult_zeroC_z; auto. elim (classic (cons_cart x2 y2 = zeroC)); intros. elim algebrique_zeroC with (a := x2) (b := y2); [ intros; try exact H1 | auto ]. rewrite H1; rewrite H2. replace (x1 * 0 + - (y1 * 0)) with 0; [ idtac | ring ]. replace (y1 * 0 + x1 * 0) with 0; [ idtac | ring ]. repeat rewrite Cmult_z_zeroC; auto. elim existence_forme_polaire with (z := cons_cart x1 y1); [ intros r1 H1; elim H1; intros a1 H2; elim H2; intros H3 H4; try clear H2 H1; try exact H4 | auto with geo ]. elim existence_forme_polaire with (z := cons_cart x2 y2); [ intros r2 H1; elim H1; intros a2 H2; elim H2; intros H5 H6; try clear H2 H1; try exact H6 | auto with geo ]. generalize (Cmult_module (cons_cart x1 y1) (cons_cart x2 y2)); intros. rewrite H5 in H1; rewrite H3 in H1. lapply (Cmult_argument (z:=cons_cart x1 y1) (z':=cons_cart x2 y2)); intros; auto with geo. rewrite H4 in H2; rewrite H6 in H2. cut (Cmult (cons_cart x1 y1) (cons_cart x2 y2) = cons_pol (r1 * r2) (a1 + a2)); intros. rewrite (polaire_calcul_algebrique (z:=Cmult (cons_cart x1 y1) (cons_cart x2 y2)) (r:=r1 * r2) (a:=a1 + a2)); auto with geo. elim passage_polaire_algebrique with (z := cons_cart x1 y1) (r := r1) (a := a1) (x := x1) (y := y1); [ intros; try exact H8 | auto with geo | auto with geo | auto with geo ]. rewrite H8; rewrite H9. elim passage_polaire_algebrique with (z := cons_cart x2 y2) (r := r2) (a := a2) (x := x2) (y := y2); [ intros | auto with geo | auto with geo | auto with geo ]. rewrite H10; rewrite H11. rewrite cos_som; rewrite sin_som. replace (r1 * r2 * (cos a1 * cos a2 + - (sin a1 * sin a2))) with (r1 * cos a1 * (r2 * cos a2) + - (r1 * sin a1 * (r2 * sin a2))); [ idtac | ring ]. replace (r1 * r2 * (sin a1 * cos a2 + sin a2 * cos a1)) with (r1 * sin a1 * (r2 * cos a2) + r1 * cos a1 * (r2 * sin a2)); [ auto | ring ]. apply forme_polaire_def; auto with geo. rewrite H2; auto. rewrite <- add_mes_compatible; auto. Qed.