proposition: Lemma le2_sums2__cong34 : forall A B C D E F A' B' C' D', Le A B A' B' -> Le C D C' D' -> SumS A B C D E F -> SumS A' B' C' D' E F -> Cong C D C' D'.
proof: Proof. intros A B C D E F A' B' C' D' HLe1 HLe2 HSum HSum'. apply le2_sums2__cong12 with A B E F A' B'; try (apply sums_sym); trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines