proposition: Lemma argument_oneC : argument oneC = image_angle 0.
proof: Proof. elim existence_forme_polaire with (z := oneC); [ 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 ]. rewrite module_oneC in H1. rewrite H2. elim passage_algebrique_argument with (z := oneC) (r := 1) (x := 1) (y := 0) (a := a); [ intros | auto with geo | auto with geo | auto with geo ]. apply egalite_angle_trigo. rewrite sin_zero; rewrite H4; ring. rewrite H3; rewrite cos_zero; field. Qed.