proposition: Lemma sums__eq34 : forall A B C D, SumS A B C D A B -> C = D.
proof: Proof. intros A B C D HSum. apply cong_identity with C. apply sums2__cong34 with A B A B; trivial. apply sums123312. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines