proposition: Lemma egalite_angle_PiPres_trigo: forall x y :R, sin x = -sin y ->cos x = -cos y -> image_angle x = image_angle (y+pi).
proof: Proof. intros x y H H0. destruct (@pi_plus_x y) as [H1 H2]. rewrite <-H2 in H. rewrite <-H1 in H0. replace (y+pi) with (pi +y);auto with real. apply egalite_angle_trigo;auto. Qed.