proposition: Lemma prop_7_8 : forall O P A B T X Y , Diam A B O P -> Bet A O T -> OnCircle X O P -> OnCircle Y O P -> LeA A O X A O Y -> Le T Y T X.
proof: Proof. intros. assert(HD:=H). unfold Diam in H. spliter. unfold OnCircle in *. induction(eq_dec_points O P). subst P. treat_equalities; auto. apply le_reflexivity. induction(eq_dec_points O T). treat_equalities. apply cong__le, cong_transitivity with O P; Cong. induction(cong_dec A X A Y). assert(X = Y \/ ReflectL X Y O A). { apply(cong_onc3_cases O P A X Y); Circle. } induction H9. treat_equalities. apply le_reflexivity. apply cong__le. apply cong_symmetry. apply cong_commutativity. apply(is_image_spec_col_cong O A X Y T); auto. unfold Diam in *. spliter. ColR. assert(Le T X T A). { apply(bet_onc_le_b O P A B T X HD H0). Circle. } assert_diffs. assert(LeA Y O T X O T). { apply lea_comm. apply(l11_36 A O X A O Y T T); auto. } assert(Lt T Y T X). { assert(Cong O X O Y) by (apply cong_transitivity with O P; Cong). apply(t18_18 O T X O T Y); Cong. unfold LtA. split; auto. intro. assert(Cong Y T X T). { apply(cong2_conga_cong Y O T X O T); Cong. } assert(CongA A O X A O Y). apply(l11_13 T O X T O Y A A); Between. CongA. apply H8. apply(cong2_conga_cong A O X A O Y); Cong. } apply lt__le. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel