proposition: Lemma pos_neg__prod_neg : forall O E E' A B C, Ps O E A -> Ng O E B -> Prod O E E' A B C -> Ng O E C.
proof: Proof. intros. assert(HP:=H1). spliter. apply prod_to_prodp in H1. unfold Prodp in H1. spliter. ex_and H3 B'. assert(HPP:= HP). unfold Prod in HP. unfold Ar2 in HP. spliter. clear H6. assert(Bet B' O E'). { apply(project_preserves_bet O E' E E' B O E B' O E'); auto. unfold Ng in H0. tauto. apply project_trivial; try(intro;subst E';apply H5; Col). Col. intro. unfold Par in H6. induction H6. { apply H6. exists E'. split; Col. } { spliter. contradiction. } unfold Proj. repeat split; try(intro;subst E';apply H5; Col). intro. unfold Par in H6. induction H6. { apply H6. exists E'. split; Col. } { spliter. contradiction. } Col. left. apply par_reflexivity. intro. subst E'. apply H5; Col. } assert(Bet A O C). { apply(project_preserves_bet O E A E' E' O B' A O C); Between. unfold Proj. repeat split; auto. intro. subst E. apply H5; Col. intro. subst A. contradiction. intro. unfold Par in H10. induction H10. { apply H10. exists A; split; Col. } { spliter. apply H5. ColR. } left. apply par_left_comm. apply par_reflexivity. intro. subst A. contradiction. apply project_trivial; Col. intro; subst E; apply H5; Col. intro;subst A;contradiction. intro. unfold Par in H10. induction H10. { apply H10. exists A. split; Col. } { spliter. apply H5; ColR. } } unfold Ng. repeat split. intro. subst C. apply prod_null in HPP. induction HPP. unfold Ps in H. unfold Out in H. tauto. subst B. unfold Ng in H0. tauto. intro. subst E. apply H5; Col. unfold Ps in H. unfold Out in H. spliter. induction H12; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order