proposition: Lemma argument_i : argument i = image_angle pisurdeux.
proof: Proof. elim existence_forme_polaire with (z := i); [ intros r H; elim H; intros a H0; elim H0; intros H1 H2; try clear H0 H existence_forme_polaire; try exact H2 | auto with geo ]. elim passage_algebrique_argument with (z := i) (r := 1) (x := 0) (y := 1) (a := a); [ intros | auto with geo | auto with geo | auto with geo ]. rewrite module_i in H1. rewrite H2. elim passage_algebrique_argument with (z := i) (r := 1) (x := 0) (y := 1) (a := a); [ intros | auto with geo | auto with geo | auto with geo ]. apply egalite_angle_trigo. rewrite sin_pisurdeux; rewrite H4; field. rewrite H3; rewrite cos_pisurdeux; ring. Qed.