|
Require Import ssreflect.
Goal forall y x : nat, x = y -> x = x.
Proof.
move=> + > ->. match goal with |- forall y, y = y => by [] end.
Qed.
Goal forall y x : nat, le x y -> x = y.
Proof.
move=> > [|].
by [].
match goal with |- forall a, _ <= a -> _ = S a => admit end.
Admitted.
Goal forall y x : nat, le x y -> x = y.
Proof.
move=> y x.
case E: x => >.
admit.
match goal with |- S _ <= y -> S _ = y => admit end.
Admitted.
¤ 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.
|
