proposition: Lemma sums2__cong12 : forall A B C D E F A' B', SumS A B C D E F -> SumS A' B' C D E F -> Cong A B A' B'.
proof: Proof. intros A B C D E F A' B' 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 Q; Cong. apply cong_transitivity with P' Q'; trivial. apply l4_3 with R R'; trivial. apply cong_transitivity with E F; Cong. apply cong_transitivity with C D; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines