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