proposition: Lemma argument_reel_neg : forall x : R, 0 > x -> argument (Rinj x) = image_angle pi.
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 ]. 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_pi; rewrite H2; ring. cut (r = - x); intros. rewrite H1; rewrite H5; rewrite cos_pi; field; trivial. rewrite <- H3. rewrite module_reel_neg in |- *; [ ring | auto with geo ]. auto with real. Qed.