proposition: Lemma argument_Conj : forall (z : C) (a : R), z <> zeroC -> argument z = image_angle a -> argument (Conj z) = image_angle (- a).
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z); intros x H1; elim H1; intros y H2; try clear H1; try exact H2. cut (Conj z = cons_cart x (- y)); intros. 2: apply Conj_def; auto. elim existence_module with (z := z); intros r H3; try clear existence_module; try exact H3. elim passage_algebrique_argument with (z := z) (r := r) (x := x) (y := y) (a := a); [ try intros; try exact H5 | auto with geo | auto with geo | auto with geo ]. cut (module (Conj z) = r); intros. elim existence_argument with (z := Conj z); [ intros b H7; try clear existence_argument; try exact H7 | auto with geo ]. elim passage_algebrique_argument with (z := Conj z) (r := r) (x := x) (y := - y) (a := b); [ try intros | auto with geo | auto with geo | auto with geo ]. rewrite H7. apply egalite_angle_trigo. rewrite H9; rewrite sin_impaire; rewrite H5; ring. rewrite H8; rewrite cos_paire; rewrite H4; ring. rewrite module_Conj; auto. Qed.