proposition: Lemma sum_assoc_1 : forall O E E' A B C AB BC ABC, Sum O E E' A B AB -> Sum O E E' B C BC -> Sum O E E' A BC ABC -> Sum O E E' AB C ABC.
proof: Proof. intros. assert(HS1:=H). assert(HS2:=H0). assert(HS3:=H1). unfold Sum in H. unfold Sum in H0. unfold Sum in H1. spliter. assert(HA1:= H). assert(HA2:= H0). assert(HA3 := H1). unfold Ar2 in H. unfold Ar2 in H0. unfold Ar2 in H1. clear H2. clear H3. clear H4. spliter. clean_duplicated_hyps. induction (eq_dec_points A O). subst A. assert(HH:= sum_O_B_eq O E E' H B AB HS1). subst AB. assert(HH:= sum_O_B_eq O E E' H BC ABC HS3). subst BC. auto. induction (eq_dec_points B O). subst B. assert(HH:= sum_A_O_eq O E E' H A AB HS1). subst AB. assert(HH:= sum_O_B_eq O E E' H C BC HS2). subst BC. auto. induction (eq_dec_points C O). subst C. assert(HH:= sum_A_O_eq O E E' H B BC HS2). subst BC. assert(HH:=sum_uniqueness O E E' A B AB ABC HS1 HS3). subst AB. apply sum_A_O; Col. assert(HH:= grid_not_par O E E' H). spliter. apply sum_comm in HS1; auto. apply sum_comm in HS3; auto. assert(S1:=HS1). assert(S2:=HS2). assert(S3:=HS3). unfold Sum in HS1. unfold Sum in HS2. unfold Sum in HS3. spliter. ex_and H20 B1'. ex_and H21 A1. ex_and H18 B1''. ex_and H25 C1. ex_and H16 BC3'. ex_and H29 A3. assert(B1'=B1''). apply (pj_uniqueness O E E' B B1' B1''); Col. subst B1''. clean_duplicated_hyps. assert(HH:=sum_par_strict O E E' H B A AB B1' A1 H19 H1 H20 H21 H22 H23 H24). spliter. assert(Par_strict O E B1' A1). induction H25. auto. contradiction. clear H25. clear H22. assert(HH:=grid_not_par O E E' H). spliter. assert(exists ! P' : Tpoint, Proj AB P' O E' E E'). apply(project_existence AB O E' E E' H37 H36). intro. apply H34. Par. ex_and H38 AB2'. unfold unique in H39. spliter. clear H39. unfold Proj in H38. spliter. clean_duplicated_hyps. assert(A <> AB). intro. subst AB. apply sum_A_B_B in S1. contradiction. auto. assert(ABC <> AB). intro. subst ABC. assert(HP := sum_uniquenessA O E E' H A BC B AB S3 S1). subst BC. apply sum_A_B_A in S2; auto. assert(HH:=plg_existence C O AB2' H2). ex_and HH C2. induction H42. assert(AB <> AB2'). intro. subst AB2'. apply par_distincts in H35. tauto. assert(Pl:=H34). assert(O <> AB2'). intro. subst AB2'. assert(HH:=plg_trivial C O H2). assert(HP:= plg_uniqueness C O O C C2 HH Pl). subst C2. induction H35. apply H35. exists E. split; Col. spliter. contradiction. apply plg_par in H34; auto. spliter. repeat split; Col. exists AB2'. exists C2. repeat split. left; Par. Col. left. apply (par_trans _ _ O C);Par. right. repeat split; Col. left. apply (par_trans _ _ O AB2'); Par. right. repeat split; Col. assert(Parallelogram O BC ABC A). right. apply(sum_cong O E E' H BC A ABC S3);auto. assert(Parallelogram O B AB A). right. apply(sum_cong O E E' H B A AB S1); auto. assert(Parallelogram O B BC C ). right. apply(sum_cong O E E' H B C BC); auto. assert( Parallelogram B AB ABC BC \/ B = AB /\ A = O /\ BC = ABC /\ B = BC). apply(plg_pseudo_trans B AB A O BC ABC). apply plg_permut. assumption. apply plg_permut. apply plg_permut. apply plg_permut. assumption. assert(Parallelogram B AB ABC BC). induction H43. assumption. spliter. contradiction. clear H43. assert(Parallelogram O C ABC AB \/ O = C /\ BC = B /\ AB = ABC /\ O = AB). apply(plg_pseudo_trans O C BC B AB ABC). apply plg_permut. apply plg_comm2. assumption. apply plg_permut. apply plg_permut. apply plg_permut. assumption. assert(Parallelogram O C ABC AB). induction H43. assumption. spliter. subst C. tauto. clear H43. assert(Parallelogram ABC AB AB2' C2 \/ ABC = AB /\ O = C /\ C2 = AB2' /\ ABC = C2). apply(plg_pseudo_trans ABC AB O C C2 AB2'). apply plg_permut. apply plg_permut. assumption. apply plg_comm2. assumption. assert(Parallelogram ABC AB AB2' C2). induction H43. assumption. spliter. subst C. tauto. clear H43. apply plg_par in H46; auto. spliter. left. apply(par_trans _ _ AB AB2'); Par. subst AB2'. assert(AB = O). apply(l6_21 O E E' O); Col. subst AB. assert(HH:= plg_trivial C O H2). assert(Hp:= plg_uniqueness C O O C C2 HH H34). subst C2. assert(Parallelogram_flat O B BC C). apply(sum_cong O E E' H B C BC);auto. assert(Parallelogram_flat O BC ABC A). apply(sum_cong O E E' H BC A ABC);auto. assert(Parallelogram_flat O B O A). apply(sum_cong O E E' H B A O); auto. assert(Parallelogram BC C A O \/ BC = C /\ O = B /\ O = A /\ BC = O). apply(plg_pseudo_trans BC C O B O A). apply plg_permut. apply plg_permut. right; assumption. right; assumption. assert(Parallelogram BC C A O). induction H38. assumption. spliter. subst A. tauto. clear H38. assert(Parallelogram O BC ABC A). right; assumption. apply plg_permut in H38. apply plg_permut in H38. apply plg_permut in H38. apply plg_permut in H39. apply plg_permut in H39. assert(HP:=plg_uniqueness A O BC C ABC H39 H38). subst ABC. apply sum_O_B; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg