proposition: Lemma ps_le : forall O E E' X, ~ Col O E E' -> Bet O X E \/ Bet O E X -> LeP O E E' O X.
proof: Proof. intros O E E' X HNC HBet. elim (eq_dec_points O X); intro HOX; [right; auto|left]. exists X; split; [apply diff_A_O; induction HBet; Col|]. assert_diffs; repeat (split; Col). Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod