proposition: Lemma sum_assoc_2 : 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' AB C ABC -> Sum O E E' A BC 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. unfold Ar2 in H. spliter. clean_duplicated_hyps. apply sum_comm; auto. apply(sum_assoc_1 O E E' C B A BC AB ABC ). apply sum_comm; auto. apply sum_comm; auto. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg