proposition: Lemma reflexion_isocele2 : forall A B M M' : PO, A <> B -> M' = reflexion A B M -> isocele B M M'.
proof: Proof. intros. apply reflexion_isocele with A; auto. apply axe_reflexion_droite with B; auto with geo. Qed.