proposition: Lemma le2_sums2__le12 : forall A B C D E F A' B' C' D' E' F', Le C' D' C D -> Le E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' -> Le A B A' B'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HLe1 HLe2 HSum HSum'. apply nlt__le; intro HLt. apply le__nlt in HLe2; apply HLe2. apply le_lt12_sums2__lt with A' B' C' D' A B C D; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines