proposition: Lemma sums_assoc_2 : forall A B C D E F G H I J K L, SumS A B C D G H -> SumS C D E F I J -> SumS A B I J K L -> SumS G H E F K L.
proof: Proof. intros A B C D E F G H I J K L HSumS1 HSumS2 HSumS3. apply sums_sym, sums_assoc_1 with C D A B I J; apply sums_sym; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines