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