proposition: Lemma bet2_le2__le : forall O o A B a b, Bet a o b -> Bet A O B -> Le o a O A -> Le o b O B -> Le a b A B.
proof: Proof. intros. induction(eq_dec_points A O). treat_equalities; auto. assert (o=a). apply le_zero with A;auto. subst;auto. induction(eq_dec_points B O). treat_equalities;auto. assert (o=b). apply le_zero with B;auto. subst;auto using le_left_comm, le_right_comm. assert(HH:= segment_construction A O b o). ex_and HH b'. assert(HH:= segment_construction B O a o). ex_and HH a'. unfold Le in H1. ex_and H1 a''. assert(a' = a''). { apply(construction_uniqueness B O a o a' a'' H4); eBetween. Cong. } treat_equalities. assert(Le B a' B A). { unfold Le. exists a'. split; eBetween; Cong. } unfold Le in H2. ex_and H2 b''. assert(b' = b''). { apply(construction_uniqueness A O b o b' b'' H3); eBetween. Cong. } treat_equalities. assert(Le a' b' a' B). { unfold Le. exists b'. split; eBetween; Cong. } assert(Le a' b' A B). { apply(le_transitivity a' b' a' B A B); auto using le_left_comm, le_right_comm. } apply(l5_6 a' b' A B a b A B); Cong. apply (l2_11 a' O b' a o b); eBetween; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col