proposition: Lemma proj_preserves_prod : forall O E E' A B C A' B' C', Prod O E E' A B C -> Ar1 O E' A' B' C' -> Pj E E' A A' -> Pj E E' B B' -> Pj E E' C C' -> Prod O E' E A' B' C'.
proof: Proof. intros. assert(Ar2 O E E' A B C). unfold Prod in H. tauto. assert(AR2:= H4). destruct H4. spliter. unfold Ar1 in H0. spliter. induction(eq_dec_points A O). subst A. assert(A' = O). eapply (pj_uniqueness O E E' O); Col. apply pj_trivial. subst A'. assert(C = O). assert(HH:= prod_0_l O E E' B H4 H6). apply(prod_uniqueness O E E' O B); auto. subst C. induction H3. apply False_ind. induction H3. apply H3. exists E'. spliter. split; Col. spliter. apply H4. ColR. subst C'. apply prod_0_l; Col. induction(eq_dec_points B O). subst B. assert(B' = O). apply (pj_uniqueness O E E' O); Col. apply pj_trivial. subst B'. assert(C = O). assert(HH:= prod_0_r O E E' A H4 H5). apply(prod_uniqueness O E E' A O); auto. subst C. induction H3. apply False_ind. induction H3. apply H3. exists E'. spliter. split; Col. spliter. apply H4. ColR. subst C'. apply prod_0_r; Col. induction(eq_dec_points C O). subst C. apply prod_null in H. induction H; contradiction. induction(eq_dec_points A' O). subst A'. apply False_ind. induction H1. induction H1. apply H1. exists E. split; Col. spliter. apply H4. ColR. contradiction. induction(eq_dec_points B' O). subst B'. apply False_ind. induction H2. induction H2. apply H2. exists E. split; Col. spliter. apply H4. ColR. contradiction. induction(eq_dec_points C' O). subst C'. apply False_ind. induction H3. induction H3. apply H3. exists E. split; Col. spliter. apply H4. ColR. contradiction. unfold Ar1 in H0. spliter. unfold Prod in *. spliter. unfold Ar2 in H. spliter. repeat split; Col. ex_and H17 B''. assert(B' = B''). apply(pj_uniqueness O E E' B B' B''); Col. subst B''. exists B. repeat split; Col. apply pj_comm. assumption. left. apply par_comm. assert(HH:= grid_not_par O E E' H4). spliter. apply(l13_19 E' A A' E B' C C' B O); Col. intro. apply H4. ColR. ColR. ColR. induction H22. assumption. subst B'. apply False_ind. apply H4. ColR. induction H2. Par. subst B'. apply False_ind. apply H4. ColR. induction H1. induction H3. apply (par_trans _ _ E E'); Par. subst C'. apply False_ind. apply H4. ColR. subst A'. apply False_ind. apply H4. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum