proposition: Lemma Prop_7_8_uniqueness : forall O P A X Y Z T, T <> O -> X <> Y -> Bet A O T -> Cong T X T Y -> Cong T X T Z -> OnCircle A O P -> OnCircle X O P -> OnCircle Y O P -> OnCircle Z O P -> Z = X \/ Z = Y.
proof: Proof. intros. induction(eq_dec_points O P). unfold OnCircle in *. treat_equalities. auto. assert(X = Y \/ ReflectL X Y O A). { apply(bet_cong_onc3_cases O P A X Y T); auto. } assert(X = Z \/ ReflectL X Z O A). { apply(bet_cong_onc3_cases O P A X Z T); auto. } assert(Y = Z \/ ReflectL Y Z O A). { apply(bet_cong_onc3_cases O P A Y Z T); auto. apply cong_transitivity with T X; Cong. } induction H9. contradiction. induction H10. auto. induction H11. auto. assert(HH:=l10_2_uniqueness_spec O A Z X Y H10 H11). contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel