blob: 8dc0c6cf0b2fd5716e8d436fdbc47b4f7c9dea6e (
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
|
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.
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 homotop : forall x : nat, forall e : x = x, e = e -> True.
Proof.
move=> >eq_ee.
lazymatch goal with
| |- True => done
end.
Qed.
|
