proposition: Lemma image_bipoint_distinct : forall (I A B A' B' : PO) (a : R), A <> B :>PO -> A' = rotation I a A -> B' = rotation I a B -> A' <> B' :>PO.
proof: Proof. intros. generalize (rotation_isometrie (I:=I) (A:=A) (B:=B) (A':=A') (B':=B') (a:=a)); intros H7. apply (isometrie_distinct (A:=A) (B:=B)); auto. symmetry in |- *; auto. Qed.