proposition: Lemma rotation_angle_nul : forall I A : PO, A = rotation I 0 A.
proof: Proof. intros. elim (classic (I = A)); intros. rewrite <- H. apply rotation_def_centre. apply rotation_def2; auto. apply angle_nul; auto. Qed.