proposition: Lemma sums_assoc_1 : 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 HSumS3. destruct HSumS1 as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]]. destruct (segment_construction P R E F) as [S [HS1 HS2]]. exists P, Q, S; repeat split; trivial. - apply between_exchange4 with R; trivial. - apply (sums2__cong56 C D E F); trivial. exists Q, R, S; repeat split; Cong. apply between_exchange3 with P; trivial. - apply (sums2__cong56 G H E F); trivial. exists P, R, S; repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines