proposition: Lemma reflexion_image_bipoint_distinct : 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. generalize (@reflexion_isometrie M N A A' B B'); intros H7. apply (isometrie_distinct (A:=A) (B:=B)); auto. Qed.