blob: b0985a0d2fc9a5c4801148ffa6d7f67ecb7d0409 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
Require Import ssreflect.
Axiom odd : nat -> Prop.
Lemma simple :
forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True.
Proof.
move=> >x_ge_3 >xy_odd.
lazymatch goal with
| |- ?x = ?y -> True => done
end.
Qed.
Lemma simple2 :
forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True.
Proof.
move=> >; move=>x_ge_3; move=> >; move=>xy_odd.
lazymatch goal with
| |- ?x = ?y -> True => done
end.
Qed.
Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True.
Lemma harder : forall x, stuff x.
Proof.
move=> >x_ge_3 >xy_odd.
lazymatch goal with
| |- ?x = ?y -> True => done
end.
Qed.
Lemma harder2 : forall x, stuff x.
Proof.
move=> >; move=>x_ge_3;move=> >; move=>xy_odd.
lazymatch goal with
| |- ?x = ?y -> True => done
end.
Qed.
Lemma homotop : forall x : nat, forall e : x = x, e = e -> True.
Proof.
move=> >eq_ee.
lazymatch goal with
| |- True => done
end.
Qed.
|
