blob: a50984c7c0676b978605458a3dfbf4322179edee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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.
|
