proposition: Lemma le2_sums2__le : forall A B C D E F A' B' C' D' E' F', Le A B A' B' -> Le C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E' F' -> Le E F E' F'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HLe1 HLe2 HSumS HSumS'. destruct HSumS as [P [Q [R [HBet [HCong1 [HCong2 HCong3]]]]]]. destruct HSumS' as [P' [Q' [R' [HBet' [HCong1' [HCong2' HCong3']]]]]]. apply (l5_6 P R P' R'); trivial. apply bet2_le2__le1346 with Q Q'; trivial. apply (l5_6 A B A' B'); Cong. apply (l5_6 C D C' D'); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines