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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
Require Import ZArith.
Require Import Lia.
Open Scope Z_scope.
Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
Proof.
intros.
lia.
Qed.
Lemma two_x_y_eq_1 : forall x y, 2 * x + 2 * y = 1 -> False.
Proof.
intros.
lia.
Qed.
Lemma two_x_y_z_eq_1 : forall x y z, 2 * x + 2 * y + 2 * z= 1 -> False.
Proof.
intros.
lia.
Qed.
Lemma unused : forall x y, y >= 0 /\ x = 1 -> x = 1.
Proof.
intros x y.
lia.
Qed.
Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False.
Proof.
intros ; intuition auto.
lia.
Qed.
Lemma compact_proof : forall z,
(z < 0) ->
(z >= 0) ->
(0 >= z \/ 0 < z) -> False.
Proof.
intros.
lia.
Qed.
Lemma dummy_ex : exists (x:Z), x = x.
Proof.
eexists.
lia.
Unshelve.
exact Z0.
Qed.
Lemma unused_concl : forall x,
False -> x > 0 -> x < 0.
Proof.
intro.
lia.
Qed.
Lemma unused_concl_match : forall (x:Z),
False -> match x with
| Z0 => True
| _ => x = x
end.
Proof.
intros.
lia.
Qed.
Lemma fresh : forall (__arith : Prop),
__arith -> True.
Proof.
intros.
lia.
Qed.
Class Foo {x : Z} := { T : Type ; dec : T -> Z }.
Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y
< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
Proof.
intros.
lia.
Qed.
Section S.
Variables x y: Z.
Variables XGe : x >= 0.
Variables YGt : y > 0.
Variables YLt : y < 0.
Goal False.
Proof using - XGe.
lia.
Qed.
Goal False.
Proof using YGt YLt x y.
lia.
Qed.
End S.
(* Bug 5073 *)
Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
Proof.
lia.
Qed.
Lemma ex_pos : forall x, exists z t, x = z - t /\ z >= 0 /\ t >= 0.
Proof.
intros.
destruct (dec_Zge x 0).
exists x, 0.
lia.
exists 0, (-x).
lia.
Qed.
Goal forall
(b q r : Z)
(H : b * q + r <= 0)
(H5 : - b < r)
(H6 : r <= 0)
(H2 : 0 <= b),
b = 0 -> False.
Proof.
intros b q r.
lia.
Qed.
|
