proposition: Lemma cong_onc3_cases : forall O P A X Y, Cong A X A Y -> OnCircle A O P -> OnCircle X O P -> OnCircle Y O P -> X = Y \/ ReflectL X Y O A.
proof: Proof. intros. unfold OnCircle in *. induction(eq_dec_points X Y). left; auto. right. assert(HH:= midpoint_existence X Y). ex_and HH M. assert(Per O M X). { apply(mid_onc2__per O P X Y M); Circle. } assert(Per A M X). { unfold Per. exists Y. split; auto. } assert(Col A O M). { apply (per2__col _ _ X); auto. intro. treat_equalities; tauto. } unfold ReflectL. split. exists M. split; Midpoint. Col. left. unfold Midpoint in *. spliter. induction(eq_dec_points M O). subst M. apply per_perp_in in H6. apply perp_in_comm in H6. apply perp_in_perp in H6. apply perp_sym in H6. apply (perp_col X O O A Y) in H6; Col. Perp. intro. treat_equalities; tauto. intro. treat_equalities; tauto. apply(perp_col O M Y X A);Col. intro. treat_equalities; tauto. apply per_perp_in in H5. apply perp_in_comm in H5. apply perp_in_perp in H5. apply perp_sym in H5. apply(perp_col X M M O Y) in H5; auto. Perp. Col. auto. intro. treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel