proposition: Lemma eq_sums__eq : forall A B C D E, SumS A B C D E E -> A = B /\ C = D.
proof: Proof. intros A B C D E HSumS. split; apply le_zero with E; [apply sums__le1256 with C D|apply (sums__le3456 A B)]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines