proposition: Lemma onc2__cong : forall O P A B, OnCircle A O P -> OnCircle B O P -> Cong O A O B.
proof: Proof. unfold OnCircle. intros O P A B H1 H2. apply cong_transitivity with O P; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel