proposition: Lemma sums_diff_1 : forall A B C D E F, A <> B -> SumS A B C D E F -> E <> F.
proof: Proof. intros A B C D E F Hdiff HSumS Heq. subst F. apply Hdiff. destruct (eq_sums__eq A B C D E HSumS); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines