Kombinatorische Konstruktionen mit Beweisen und Schnittelimination