proposition: Lemma pos_not_neg : forall O E A, Ps O E A -> ~Ng O E A.
proof: Proof. intros. intro. unfold Ps in H. unfold Ng in H0. unfold Out in H. spliter. induction H4. apply H. apply (between_equality _ _ E); Between. apply H1. apply (between_equality _ _ A); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod