proposition: Lemma sums2__cong34 : forall A B C D E F 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 C' D' HSumS HSumS'. apply sums2__cong12 with A B E F; apply sums_sym; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines