proposition: Lemma onc_sym__onc : forall O P A B X Y, Bet O A B -> OnCircle A O P -> OnCircle B O P -> OnCircle X O P -> ReflectL X Y A B -> OnCircle Y O P.
proof: Proof. intros. unfold OnCircle in *. assert(Cong X O Y O). { apply(is_image_spec_col_cong A B X Y O H3);Col. } apply cong_transitivity with O X; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel