proposition: Lemma prod_assoc1 : 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' A BC ABC -> Prod O E E' AB C 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' A BC 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' BC H2 H10). assert(ABC=O). apply(prod_uniqueness O E E' O BC); assumption. subst ABC. apply prod_0_l; assumption. induction(eq_dec_points B O). subst B. assert(HH:=prod_0_r O E E' A H2 H11). assert(AB = O). apply(prod_uniqueness O E E' A O); assumption. subst AB. assert(HP:=prod_0_l O E E' C H2 H9). assert(BC=O). apply(prod_uniqueness O E E' O C); assumption. subst BC. assert(ABC=O). apply(prod_uniqueness O E E' A O); assumption. subst ABC. apply prod_0_l; assumption. induction(eq_dec_points C O). subst C. assert(HH:=prod_0_r O E E' B H2 H12). assert(BC = O). apply(prod_uniqueness O E E' B O); assumption. subst BC. assert(HP:=prod_0_r O E E' A H2 H11). assert(ABC=O). apply(prod_uniqueness O E E' A O); assumption. subst ABC. 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(exists ! P', Proj C P' O E' E E'). apply(project_existence C O E' E E' H20 H19); Par. ex_and H21 C'. unfold unique in H22. spliter. clear H22. unfold Proj in H21. spliter. clean_duplicated_hyps. assert(Par C C' E E'). induction H25. assumption. subst C'. apply False_ind. apply H2. ColR. clear H25. exists C'. repeat split. left. Par. Col. ex_and H14 B'. ex_and H8 C''. assert(C' = C''). apply(pj_uniqueness O E E' C); Col. left. Par. subst C''. ex_and H6 BC'. assert(B' <> O). intro. subst B'. induction H14. apply H15. apply par_symmetry. apply(par_col_par _ _ _ B); Par; Col. contradiction. assert(BC <> O). intro. subst BC. assert(HH:=prod_null O E E' B C P2). induction HH; contradiction. left. apply(l13_19 B' B E' AB BC' BC C' ABC O); Col. intro. apply H2. ColR. intro. subst BC'. induction H6. apply H15. apply par_symmetry. apply (par_col_par _ _ _ BC); Par; Col. contradiction. intro. subst C'. apply H15. apply par_symmetry. apply (par_col_par _ _ _ C); Par; Col. intro. subst AB. assert(HH:=prod_null O E E' A B P1). induction HH; contradiction. intro. subst ABC. assert(HH:=prod_null O E E' A BC P3). induction HH; contradiction. ColR. ColR. ColR. ColR. ColR. induction H14. induction H6. apply (par_trans _ _ E E'); Par. subst BC'. apply False_ind. apply H2. ColR. subst B'. apply False_ind. apply H2. ColR. induction H23. induction H28. apply (par_trans _ _ E' A); Par. subst BC'. apply False_ind. apply H2. assert(ABC <> O). intro. subst ABC. assert(HH:=prod_null O E E' A BC P3). induction HH; contradiction. ColR. subst AB. apply False_ind. apply H2. ColR. induction H26. Par. subst BC. apply False_ind. apply H2. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum