| 1004 |
2019/11/09 22:00:05
|
n < m \/ n = m \/ n > m
|
lo48576 |
Success |
|
|
| 1003 |
2019/11/09 20:22:48
|
Three is prime
|
lo48576 |
Success |
|
|
| 1002 |
2019/11/09 15:52:44
|
Boolean-hole principle
|
lo48576 |
Success |
|
|
| 1001 |
2019/11/09 15:49:14
|
Boolean-hole principle
|
lo48576 |
Success |
|
|
| 1000 |
2019/11/09 04:05:18
|
De Morgan's laws in Coq
|
lo48576 |
Success |
|
|
| 999 |
2019/11/09 02:07:44
|
mult_n_O
|
lo48576 |
Success |
|
|
| 998 |
2019/11/09 02:00:36
|
gcd(n, n+1) = 1
|
lo48576 |
Success |
|
|
| 997 |
2019/11/08 03:36:46
|
Summand of one
|
lo48576 |
Success |
|
|
| 996 |
2019/11/08 02:54:03
|
forall l: list nat, l @ [0] <> []
|
lo48576 |
Success |
|
|
| 995 |
2019/11/08 02:50:23
|
forall l: list nat, l @ [0] <> []
|
lo48576 |
Failure |
|
|
| 994 |
2019/11/07 23:16:42
|
n * S m = n + n * m
|
lo48576 |
Success |
|
|
| 993 |
2019/11/07 21:15:46
|
Definitions of injectivity
|
na4zagin3 |
Success |
|
|
| 992 |
2019/11/07 21:13:42
|
Definitions of injectivity
|
nuip |
Failure |
|
|
| 991 |
2019/11/07 20:37:25
|
Multiplication in F_2 is idempotent
|
na4zagin3 |
Success |
|
|
| 990 |
2019/11/07 20:37:01
|
Multiplication in F_2 is idempotent
|
na4zagin3 |
Failure |
|
|
| 989 |
2019/11/07 20:09:28
|
Multiplication in F_2 is idempotent
|
na4zagin3 |
Failure |
|
|
| 988 |
2019/11/07 20:05:22
|
Multiplication in F_2 is idempotent
|
nuip |
Failure |
|
|
| 987 |
2019/11/07 19:46:45
|
Multiplication in F_2 is idempotent
|
yodvhskd |
Success |
|
|
| 986 |
2019/11/07 19:33:35
|
Cumulative sum of list
|
nekodesu |
Failure |
|
|
| 985 |
2019/11/07 19:22:49
|
forall f: bool -> bool, f^3(x) = f(x)
|
lo48576 |
Success |
|
|
| 984 |
2019/11/07 17:36:01
|
plus_comm
|
lo48576 |
Success |
|
|
| 983 |
2019/11/07 17:11:20
|
1 + 1 = 2
|
lo48576 |
Success |
|
|
| 982 |
2019/11/07 16:58:51
|
plus_comm
|
lo48576 |
Success |
|
|
| 981 |
2019/11/07 15:33:17
|
plus_assoc
|
lo48576 |
Success |
|
|
| 980 |
2019/11/07 15:27:50
|
plus_assoc
|
lo48576 |
Success |
|
|
| 979 |
2019/11/06 23:58:13
|
Product of n consecutive integers is divisible by n!
|
yodvhskd |
Success |
|
|
| 978 |
2019/11/05 23:55:09
|
l1 <> l2 if l2 is an odd permutation of l1
|
yodvhskd |
Success |
|
|
| 977 |
2019/11/05 12:53:39
|
n * S m = n + n * m
|
saitou |
Success |
|
|
| 976 |
2019/11/05 12:53:09
|
n * S m = n + n * m
|
saitou |
Success |
|
|
| 975 |
2019/11/05 12:36:33
|
forall f: bool -> bool, f^3(x) = f(x)
|
saitou |
Success |
|
|
| 974 |
2019/11/05 12:23:52
|
1 + 1 = 2
|
saitou |
Success |
|
|
| 973 |
2019/11/05 12:22:53
|
plus_comm
|
saitou |
Success |
|
|
| 972 |
2019/11/05 12:13:41
|
plus_assoc
|
saitou |
Success |
|
|
| 971 |
2019/11/04 22:01:49
|
plus_comm
|
CoiL |
Failure |
|
|
| 970 |
2019/11/04 20:54:24
|
Sum of binomial coefficients
|
yodvhskd |
Success |
|
|
| 969 |
2019/11/04 20:44:39
|
Sum of binomial coefficients
|
yodvhskd |
Failure |
|
|
| 968 |
2019/11/04 20:40:13
|
Sum of binomial coefficients
|
yodvhskd |
Failure |
|
|
| 967 |
2019/11/04 04:34:31
|
Yoneda embedding for preorder
|
ukikagi |
Success |
|
|
| 966 |
2019/11/03 19:57:59
|
mult_n_O
|
egashira |
Success |
|
|
| 965 |
2019/11/03 19:56:29
|
Double
|
egashira |
Success |
|
|
| 964 |
2019/11/01 12:33:30
|
n < m \/ n = m \/ n > m
|
chy |
Success |
|
|
| 963 |
2019/11/01 11:17:15
|
Sum of binomial coefficients
|
chy |
Success |
|
|
| 962 |
2019/11/01 11:16:29
|
Sum of binomial coefficients
|
chy |
Failure |
|
|
| 961 |
2019/11/01 11:15:32
|
Sum of binomial coefficients
|
chy |
Failure |
|
|
| 960 |
2019/10/31 23:22:12
|
Sum of binomial coefficients
|
nuip |
Failure |
|
|
| 959 |
2019/10/31 22:39:21
|
Double
|
chy |
Success |
|
|
| 958 |
2019/10/31 22:14:45
|
Yoneda embedding for preorder
|
chy |
Success |
|
|
| 957 |
2019/10/31 20:38:57
|
Identity permutation
|
CoiL |
Success |
|
|
| 956 |
2019/10/31 20:16:52
|
1 + 1 = 2
|
sh_mug |
Success |
|
|
| 955 |
2019/10/31 20:12:24
|
plus_comm
|
sh_mug |
Success |
|
|