proposition: Lemma rotation_image_bipoint_coincide : forall (I A B A' B' :PO) ( a : R), A' = rotation I a A -> B' = rotation I a B -> A =B -> A' = B'.
proof: Proof. intros I A B A' B' a H H0 H1. rewrite ->H1 in H. rewrite <-H0 in H. assumption. Qed.