Require Import ArithRing.
Lemma l1 : 2 = 1 + 1.
ring.
Qed.
Lemma l2 : forall x : nat, S (S x) = 1 + S x.
intro.
ring.
Qed.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|