proposition: Lemma le_lt56_sums2__lt34 : forall A B C D E F A' B' C' D' E' F', Le A' B' A B -> Lt E F E' F' -> SumS A B C D E F -> SumS A' B' C' D' E' F' -> Lt C D C' D'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HLe HLt HSum HSum'. apply le_lt56_sums2__lt12 with A B E F A' B' E' F'; try (apply sums_sym); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines