proposition: Lemma bet2_lt_le__lt : forall O o A B a b : Tpoint, Bet a o b -> Bet A O B -> Cong o a O A -> Lt o b O B -> Lt a b A B.
proof: Proof. intros. unfold Lt. split. unfold Lt in *. spliter. assert(Le o a O A). { unfold Le. exists A. split; Between. } apply(bet2_le2__le O o A B a b); auto. intro. assert(HH:=segment_construction A O o b). ex_and HH b'. unfold Lt in H2. spliter. apply H6. apply(l4_3_1 a o b A O B H H0 ); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR