proposition: Lemma reflexion_image_bipoint_coincide : forall (M N A B A' B' :PO), M<>N-> A' = reflexion M N A -> B' = reflexion M N B -> A =B -> A' = B'.
proof: Proof. intros M N A B A' B' H H0 H1 H2. rewrite ->H2 in H0. rewrite <-H1 in H0. assumption. Qed.