proposition: Lemma argument_reel_pos : forall x : R, 0 < x -> argument (Rinj x) = image_angle 0.
proof: Proof. intros. cut (x <> 0); intros. elim existence_forme_polaire with (z := Rinj x); [ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1; try exact H4 | auto with geo ]. cut (x = r); intros. elim passage_algebrique_argument with (z := Rinj x) (r := r) (x := x) (y := 0) (a := a); [ intros | auto with geo | auto with geo | auto with geo ]. rewrite H4. apply egalite_angle_trigo. rewrite sin_zero; rewrite H5; ring. rewrite H2; rewrite <- H1; rewrite cos_zero; field; trivial. rewrite module_reel_pos in H3; auto. lra. auto with real. Qed.