proposition: Lemma lt2_sums2__lt12 : forall A B C D E F A' B' C' D' E' F', Lt C' D' C D -> Lt E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' -> Lt A B A' B'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HLt1 HLt2 HSum HSum'. apply le_lt56_sums2__lt12 with C D E F C' D' E' F'; Le. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines