proposition: Lemma bet2_lt2__lt : forall O o A B a b : Tpoint, Bet a o b -> Bet A O B -> Lt o a O A -> Lt o b O B -> Lt a b A B.
proof: Proof. intros. unfold Lt. split. unfold Lt in *. spliter. apply(bet2_le2__le O o A B a b); auto. intro. induction(eq_dec_points O A). treat_equalities. unfold Lt in H1. spliter. apply le_zero in H0. treat_equalities. apply H1. apply cong_trivial_identity. induction(eq_dec_points O B). treat_equalities. unfold Lt in H2. spliter. apply le_zero in H0. treat_equalities. apply H2. apply cong_trivial_identity. unfold Lt in *. spliter. unfold Le in H1. ex_and H1 a'. unfold Le in H2. ex_and H2 b'. assert(Bet a' O b'). apply between_inner_transitivity with B. apply between_exchange3 with A. Between. assumption. Between. assert(Cong a b a' b'). { apply (l2_11 a o b a' O b'); Cong. } assert(Cong a' b' A B) by (apply cong_transitivity with a b; Cong). assert(Bet A b' B) by eBetween. induction(eq_dec_points A a'). treat_equalities. assert(b'=B \/ Midpoint A b' B). { apply l7_20. Col. Cong. } induction H1. treat_equalities. contradiction. unfold Midpoint in *. spliter. assert(b' = B). { apply (between_cong A). Between. Cong. } treat_equalities; tauto. assert(Bet B a' A) by eBetween. induction(eq_dec_points B b'). treat_equalities. assert(a'=A \/ Midpoint B a' A). { apply l7_20. Col. Cong. } induction H2. treat_equalities. contradiction. unfold Midpoint in *. spliter. assert(a' = A). { apply (between_cong B). Between. Cong. } treat_equalities; tauto. assert(Bet a' A b' \/ Bet a' B b'). { apply(col_cong_bet A B a' b'). Col. Cong. eBetween. } induction H17. assert(A = a'). { apply(between_equality _ _ b'). apply between_exchange4 with O. Between. apply between_inner_transitivity with B. assumption. assumption. assumption. } treat_equalities; tauto. assert(b' = B). { apply(between_equality _ _ a'). Between. apply between_exchange4 with O. Between. apply between_inner_transitivity with A. Between. Between. } treat_equalities; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR