proposition: Lemma argument_opp_un : argument (Rinj (-1)) = image_angle pi.
proof: Proof. elim existence_forme_polaire with (z := Rinj (-1)); [ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1; try exact H4 | auto with geo ]. rewrite module_opp_un in H3. elim passage_algebrique_argument with (z := Rinj (-1)) (r := 1) (x := -1) (y := 0) (a := a); [ intros | auto with geo | auto with geo | auto with geo ]. rewrite H4. apply egalite_angle_trigo. rewrite sin_pi; rewrite H0; ring. rewrite H; rewrite cos_pi; field. Qed.