proposition: Lemma prod_assoc2 : forall O E E' A B C AB BC ABC, Prod O E E' A B AB -> Prod O E E' B C BC -> (Prod O E E' AB C ABC -> Prod O E E' A BC ABC).
proof: Proof. intros. assert(Ar2 O E E' A B AB). unfold Prod in H. tauto. assert(Ar2 O E E' B C BC). unfold Prod in H0. tauto. assert(Ar2 O E E' AB C ABC). unfold Prod in H1. tauto. unfold Ar2 in *. spliter. clean_duplicated_hyps. induction(eq_dec_points A O). subst A. assert(HH:=prod_0_l O E E' B H2 H12). assert(AB = O). apply(prod_uniqueness O E E' O B); assumption. subst AB. assert(HP:=prod_0_l O E E' C H2 H9). assert(ABC=O). apply(prod_uniqueness O E E' O C); assumption. subst ABC. apply prod_0_l; assumption. induction(eq_dec_points B O). subst B. assert(HH:=prod_0_l O E E' C H2 H9). assert(BC = O). apply(prod_uniqueness O E E' O C); assumption. subst BC. assert(HP:=prod_0_r O E E' A H2 H11). assert(AB=O). apply(prod_uniqueness O E E' A O); assumption. subst AB. assert(ABC=O). apply(prod_uniqueness O E E' O C); assumption. subst ABC. apply prod_0_r; assumption. induction(eq_dec_points C O). subst C. assert(HH:=prod_0_r O E E' B H2 H12). assert(ABC=O). assert(HP:=prod_0_r O E E' AB H2 H13). apply(prod_uniqueness O E E' AB O); assumption. subst ABC. assert(BC=O). apply(prod_uniqueness O E E' B O); assumption. subst BC. apply prod_0_r; assumption. assert(P1:=H). assert(P2:= H0). assert(P3:=H1). unfold Prod in H. unfold Prod in H0. unfold Prod in H1. spliter. repeat split; auto. assert(HH:=grid_not_par O E E' H2). spliter. assert(BC <> O). intro. subst BC. apply prod_null in P2. induction P2; contradiction. assert(exists ! P', Proj BC P' O E' E E'). apply(project_existence BC O E' E E' H20 H19); Par. ex_and H22 BC'. unfold unique in H23. spliter. clear H23. unfold Proj in H22. spliter. clean_duplicated_hyps. assert(Par BC BC' E E'). induction H26. assumption. subst BC'. apply False_ind. apply H2. ColR. clear H26. exists BC'. repeat split. left. Par. Col. ex_and H14 B'. ex_and H8 C'. ex_and H6 C''. assert(C' = C''). apply(pj_uniqueness O E E' C); Col. left. subst C''. assert(B' <> O). intro. subst B'. induction H14. apply H15. apply par_symmetry. apply(par_col_par _ _ _ B); Par; Col. contradiction. apply(par_trans _ _ B' AB). induction H24. Par. subst B'. apply False_ind. apply H2. ColR. apply(l13_19 E' B B' AB C' BC BC' ABC O); auto. intro. apply H2. ColR. intro. subst C'. apply H15. apply par_symmetry. induction H6. apply(par_col_par _ _ _ C); Par. Col. contradiction. intro. subst BC'. apply H15. apply par_symmetry. apply(par_col_par _ _ _ BC); Par. Col. intro. subst AB. apply prod_null in P1. induction P1; contradiction. intro. subst ABC. apply prod_null in P3. induction P3. subst AB. apply prod_null in P1. induction P1; contradiction. contradiction. ColR. ColR. ColR. induction H27. Par. subst C'. apply False_ind. apply H15. apply par_symmetry. apply(par_col_par _ _ _ C); auto. apply par_comm. apply(par_col_par _ _ _ BC); auto. induction H6. Par. subst BC. apply False_ind. apply H2. ColR. ColR. Col. induction H29. Par. subst C'. apply False_ind. apply H2. assert(ABC <> O). intro. subst ABC. apply H15. apply par_symmetry. apply(par_col_par _ _ _ C); auto. induction H6. Par. contradiction. ColR. ColR. induction H14. apply (par_trans _ _ E E'); Par. subst B'. apply False_ind. apply H2. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum