Section test. Variable n:nat. Lemma foo: 0 <= n. Proof. (* declaring an Axiom during a proof makes it immediately
usable, juste as a full Definition. *) Axiom bar : n = 1. rewrite bar. nowapply le_S. Qed.
Lemma foo' : 0 <= n. Proof. (* Declaring an Hypothesis during a proof is ok, but this hypothesis won't be usable by the current proof(s),
only by later ones. *) Hypothesis bar' : n = 1.
Fail rewrite bar'. Abort.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
