proposition: Lemma prod_pos_pos : forall O E E' A B AB, Ps O E A -> Ps O E B -> Prod O E E' A B AB -> Ps O E AB.
proof: Proof. intros. assert(HP:= H1). unfold Prod in H1. spliter. unfold Ar2 in H1. spliter. ex_and H2 B'. assert(HG:= grid_not_par O E E' H1). spliter. unfold Ps in H. unfold Ps in H0. unfold Out in *. spliter. assert(E' <> A). intro. subst A. contradiction. assert(~Col O E' A). intro. apply H1. ColR. assert(~Par O E E' A). intro. induction H20. apply H20. exists A. split; Col. spliter. contradiction. assert(Proj E E' O E' E E'). apply(pj_col_project); Col. left; right. repeat split; Col. assert(Proj B B' O E' E E'). apply(pj_col_project); Col. assert(Proj O O O E' E E'). apply(pj_col_project); Col. right. auto. assert(Proj E' A O E E' A). apply(pj_col_project); Col. left; right. repeat split; Col. assert(Proj B' AB O E E' A). apply(pj_col_project); Col. assert(Proj O O O E E' A). apply(pj_col_project); Col. right. auto. assert(AB <> O). intro. subst AB. apply prod_null in HP. induction HP; contradiction. unfold Ps. repeat split; auto. induction H15. assert(Bet O B' E'). apply(project_preserves_bet O E' E E' O B E O B' E'); auto. assert(Bet O AB A). apply(project_preserves_bet O E E' A O B' E' O AB A); auto. induction H17. left. apply(between_exchange4 _ _ A); auto. apply(l5_3 O AB E A); auto. assert(Bet O E' B'). apply(project_preserves_bet O E' E E' O E B O E' B'); auto. assert(Bet O A AB). apply(project_preserves_bet O E E' A O E' B' O A AB); auto. induction H17. assert(Bet O E AB \/ Bet O AB E). apply(l5_1 O A E AB); auto. tauto. right. apply (between_exchange4 O E A AB); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod