proposition: Lemma signeq__prod_pos : forall O E E' A B C, SignEq O E A B -> Prod O E E' A B C -> Ps O E C.
proof: Proof. intros. unfold SignEq in H. induction H. spliter. apply (prod_pos_pos O E E' A B); auto. assert(HP:=H0). spliter. apply prod_to_prodp in H0. unfold Prodp in H0. spliter. ex_and H3 B'. assert(HPP:= HP). unfold Prod in HP. unfold Ar2 in HP. spliter. assert(Bet B' O E'). { assert(HQQ:=project_preserves_bet). apply(project_preserves_bet O E' E E' B O E B' O E'); auto. unfold Ng in H1. tauto. apply project_trivial; try(intro;subst E';apply H5; Col). Col. intro. unfold Par in H10. induction H10. { apply H10. exists E'. split; Col. } { spliter. contradiction. } unfold Proj. repeat split; try(intro;subst E';apply H5; Col). intro. unfold Par in H10. induction H10. { apply H10. 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 H11. induction H11. { apply H11. 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 H11. induction H11. { apply H11. exists A. split; Col. } { spliter. apply H5; ColR. } } unfold Ps. unfold Ng in H. spliter. apply l6_6. assert(HH:= l6_2 E C A O). apply HH; Between. intro. subst C. apply prod_null in HPP. unfold Ng in H1. spliter. induction HPP; contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order