proposition: Lemma leP_bet : forall O E E' AB CD, LeP O E E' AB CD -> LeP O E E' O AB -> LeP O E E' O CD -> Bet O AB CD.
proof: Proof. intros. unfold LeP in H. induction H. unfold LtP in H. ex_and H X. apply diff_sum in H. assert(Out O AB X \/ AB=O). unfold LeP in H0. induction H0. left. apply ltP_pos in H0. unfold Ps in *. eapply (l6_7 _ _ E); auto. apply l6_6. assumption. right. auto. induction H3. apply (l14_36_a O E E' AB X CD); auto. subst AB. apply between_trivial2. subst CD. apply between_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order