proposition: Lemma le2_sums2__cong12 : 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 A B A' B'.
proof: Proof. intros A B C D E F A' B' C' D' HLe1 HLe2 HSum HSum'. apply sums2__cong12 with C D E F; trivial. destruct (ex_sums A' B' C D) as [E' [F' HSum1]]. apply (cong3_sums__sums A' B' C D E' F'); Cong. apply le_anti_symmetry. apply le2_sums2__le with A' B' C D A' B' C' D'; Le. apply le2_sums2__le with A B C D A' B' C D; Le. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines