proposition: Lemma sums2__cong56 : forall A B C D E F E' F', SumS A B C D E F -> SumS A B C D E' F' -> Cong E F E' F'.
proof: Proof. intros A B C D E F E' F' HSumS HSumS'. destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]]. destruct HSumS' as [P' [Q' [R' [HBet' [HCong1' [HCong2' HCong3']]]]]]. apply cong_transitivity with P R; Cong. apply cong_transitivity with P' R'; trivial. apply l2_11 with Q Q'; trivial. apply cong_transitivity with A B; Cong. apply cong_transitivity with C D; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines