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