blob: 5e303a0b7f1a8e95473b226e5448e3e1b87226a8 (
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
|
From Coq Require Import Lia ZArith.ZArith NArith.NArith.
Unset Nia Cache.
Open Scope N_scope.
Lemma over (n0 n1 n2 n3 n4 n5 n6 : N)
(e0 : 1 + 8 * n0 = n1 * n1 + n2)
(e1 : n1 - 1 = 2 * n3 + n4)
(e2 : n3 * (1 + n3) = 2 * n5)
(e3 : n2 + 2 * n4 * n1 - n4 = 8 * n6)
(o0 : n4 = 0 \/ n4 = 1) :
n6 = n0 - n5.
Proof.
Time nia.
Qed.
Lemma over2 (n0 n1 n2 n3 n4 n5 n6 : N)
(e0 : 1 + 8 * n0 = n1 * n1 + n2)
(e1 : n1 + 1 = 2 * n3 + n4)
(e2 : n3 * (1 + n3) = 2 * n5)
(e3 : n2 + 2 * n4 * n1 + n4 = 8 * n6)
(o0 : n4 = 0) :
n6 = n0 + n5.
Proof.
Fail nia.
Abort.
Open Scope Z_scope.
Lemma over3 (n1 n2 n3 n4 n5 : Z)
(e : 0 <= n1 /\ 0 <= n2 /\ 0 <= n3 /\ 0 <= n4
/\ 0 <= n5)
(e1 : n1 + 1 = 20 * n3 + n4)
(e3 : n2 + 2 * n4 * n1 + n4 = 8 * n5) :
n5 = 0.
Proof.
Time Fail nia.
Abort.
|
