proposition: Lemma reflexion_isocele : forall A B M M' : PO, A <> B -> M' = reflexion A B M -> isocele A M M'.
proof: Proof. intros. elim (classic (alignes A B M)); intros. replace M' with M; auto. unfold isocele in |- *; auto. rewrite H0; rewrite <- reflexion_axe; auto. apply mediatrice_isocele. elim (reflexion_mediatrice (A:=A) (B:=B) (M:=M) (M':=M')); auto. Qed.