proposition: Lemma cong3_sums__sums : forall A B C D E F A' B' C' D' E' F', Cong A B A' B' -> Cong C D C' D' -> Cong E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HCong1 HCong2 HCong3 HSumS. destruct HSumS as [P [Q [R [HBet [HCong4 [HCong5 HCong6]]]]]]. exists P, Q, R; repeat split; trivial; eapply cong_transitivity; eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines