proposition: Lemma deux_mes_angle_rotation : forall (I M : PO) (a b : R), image_angle a = image_angle b -> rotation I a M = rotation I b M.
proof: Proof. intros. elim (classic (I = M)); intros. rewrite <- H0; repeat rewrite <- rotation_def_centre; auto. elim (existence_rotation_Ia I M a); intros. rewrite <- H1. generalize (rotation_def (I:=I) (A:=M) (B:=x) (a:=a)); intros. elim H2; auto; intros. apply rotation_def2; auto. rewrite <- H4; rewrite <- H; auto. Qed.