proposition: Lemma bet_cong_onc3_cases : forall O P A X Y T, T <> O -> Bet A O T -> Cong T X T 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 O P). treat_equalities. left; auto. induction(eq_dec_points T X). treat_equalities. left; auto. assert(CongA T O X T O Y /\ CongA O T X O T Y /\ CongA T X O T Y O). { apply(l11_51 O T X O T Y); Cong. intro. treat_equalities; tauto. apply cong_transitivity with O P; Cong. } spliter. assert(Out T A O). { repeat split; auto. intro. treat_equalities; tauto. Between. } assert(Cong A X A Y). { apply(cong2_conga_cong A T X A T Y); Cong. apply (l11_10 O T X O T Y); auto. apply out_trivial; auto. apply out_trivial. intro. treat_equalities; tauto. } apply (cong_onc3_cases O P); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel