proposition: Lemma l6_16_1 : forall P Q S X, P<>Q -> Col S P Q -> Col X P Q -> Col X P S.
proof: Proof. intros. destruct (eq_dec_points S P). subst; Col. assert((Bet P S X \/ Bet P X S) -> (Bet P S X \/ Bet S X P)) by (intro; induction H3; Between). unfold Col. induction H0;induction H1. right; apply H3; eapply (l5_2 Q P); Between. induction H1; left; eBetween. induction H0; left; eBetween. induction H0; induction H1. right; apply H3; eapply l5_1; eauto. right; right; eBetween. right; left; eBetween. right; apply H3; eapply l5_3; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le