proposition: Lemma diam_end_uniqueness : forall O P A B C, Diam A B O P -> Diam A C O P -> B = C.
proof: Proof. intros. apply diam__midpoint in H. apply diam__midpoint in H0. apply (symmetric_point_uniqueness A O); Midpoint. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel