proposition: Lemma sums_assoc : 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 G H E F K L <-> SumS A B I J K L).
proof: Proof. intros A B C D E F G H I J K L HSumS1 HSumS2. split; intro HSumS3. - apply sums_assoc_1 with C D E F G H; trivial. - apply sums_assoc_2 with A B C D I J; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines