# | Name | Publish time | Difficulty | Compiler | Source code policy | |
---|---|---|---|---|---|---|

64 | Eat the Candies | 2020/09/27 20:00:00 | 3 | Coq 8.11.1 | Public | |

63 | Perfect Square? | 2020/09/27 20:00:00 | 2 | Coq 8.11.1 | Public | |

62 | If zero were not nat | 2020/09/27 20:00:00 | 2 | Coq 8.11.1 | Public | |

61 | Flat CPO | 2020/09/27 20:00:00 | 1 | Coq 8.11.1 | Public | |

60 | Friends and strangers (corrected) | 2020/08/17 00:40:00 | 3 | Coq 8.11.1 | Public | |

59 | Friends and strangers | 2020/08/16 20:00:00 | 1 | Coq 8.11.1 | Public | |

58 | The set of all finite sequences of bool is countable | 2020/08/16 20:00:00 | 2 | Coq 8.11.1 | Public | |

57 | Fibonacci numbers modulo 2 | 2020/08/16 20:00:00 | 2 | Coq 8.11.1 | Public | |

56 | Rotate once | 2020/08/16 20:00:00 | 2 | Coq 8.11.1 | Public | |

55 | Sum of n^3 | 2020/08/16 20:00:00 | 1 | Coq 8.11.1 | Public | |

54 | Tree Syntax Unambiguity | 2020/06/14 19:00:00 | 4 | Coq 8.11.1 | Public | |

53 | Tree Induction | 2020/06/14 19:00:00 | 3 | Coq 8.11.1 | Public | |

52 | count_occ_app | 2020/06/14 19:00:00 | 2 | Coq 8.11.1 | Public | |

51 | S preserves comparison | 2020/06/14 19:00:00 | 1 | Coq 8.11.1 | Public | |

50 | Infinite duplication | 2020/05/03 20:00:00 | 3 | Coq 8.11.1 | Public | |

49 | Upper triangular (completeness) | 2020/05/03 20:00:00 | 2 | Coq 8.11.1 | Public | |

48 | Upper triangular (soundness) | 2020/05/03 20:00:00 | 2 | Coq 8.11.1 | Public | |

47 | Drinker paradox? | 2020/05/03 20:00:00 | 2 | Coq 8.11.1 | Public | |

46 | Swap twice | 2020/05/03 20:00:00 | 1 | Coq 8.11.1 | Public | |

45 | Cycle detection | 2020/03/15 20:00:00 | 4 | Coq 8.11.1 | Public | |

44 | Postorder traversal | 2020/03/15 20:00:00 | 2 | Coq 8.11.1 | Public | |

43 | Not a sum of squares | 2020/03/15 20:00:00 | 2 | Coq 8.11.1 | Public | |

42 | eq_sym? | 2020/03/15 20:00:00 | 1 | Coq 8.11.1 | Public | |

41 | and_comm (Lean) | 2020/02/05 03:15:00 | 1 | Lean 3.4.2 | Public | |

40 | Binary search | 2019/12/08 20:00:00 | 3 | Coq 8.11.1 | Public | |

39 | Boolean-hole principle revisited | 2019/12/08 20:00:00 | 2 | Coq 8.11.1 | Public | |

38 | Midpoint | 2019/12/08 20:00:00 | 1 | Coq 8.11.1 | Public | |

37 | Zero test | 2019/12/08 20:00:00 | 1 | Coq 8.11.1 | Public | |

36 | Relative prime squares | 2019/11/24 20:00:00 | 3 | Coq 8.11.1 | Public | |

35 | infinite bool sequence is uncountable | 2019/11/24 20:00:00 | 2 | Coq 8.11.1 | Public | |

34 | Tree addressing is injective | 2019/11/24 20:00:00 | 2 | Coq 8.11.1 | Public | |

33 | Constructor is injective | 2019/11/24 20:00:00 | 1 | Coq 8.11.1 | Public | |

32 | Uniqueness of inequality proofs | 2019/10/26 18:00:00 | 4 | Coq 8.11.1 | Public | |

31 | Sum of binomial coefficients | 2019/10/26 18:00:00 | 3 | Coq 8.11.1 | Public | |

30 | Double | 2019/10/26 18:00:00 | 2 | Coq 8.11.1 | Public | |

29 | Yoneda embedding for preorder | 2019/10/26 18:00:00 | 1 | Coq 8.11.1 | Public | |

28 | Iterated iteration | 2019/10/06 20:00:00 | 3 | Coq 8.11.1 | Public | |

27 | Two is not Three | 2019/10/06 20:00:00 | 2 | Coq 8.11.1 | Public | |

26 | Three is prime | 2019/10/06 20:00:00 | 1 | Coq 8.11.1 | Public | |

25 | Boolean-hole principle | 2019/10/06 20:00:00 | 1 | Coq 8.11.1 | Public | |

24 | Multiplication of non-zero value in F_p is injective | 2019/09/22 20:00:00 | 3 | Coq 8.11.1 | Public | |

23 | Any natural number is expressible in binary notation | 2019/09/22 20:00:00 | 2 | Coq 8.11.1 | Public | |

22 | De Morgan's laws in Coq | 2019/09/22 20:00:00 | 1 | Coq 8.11.1 | Public | |

21 | mult_n_O | 2019/09/22 20:00:00 | 1 | Coq 8.11.1 | Public | |

20 | Grand Garden | 2019/09/15 17:00:00 | 3 | Coq 8.11.1 | Public | |

19 | unique count | 2019/09/15 17:00:00 | 2 | Coq 8.11.1 | Public | |

18 | unique (unique l) = l | 2019/09/15 17:00:00 | 2 | Coq 8.11.1 | Public | |

17 | count l n = count (rev l) n | 2019/09/15 17:00:00 | 2 | Coq 8.11.1 | Public | |

16 | gcd(n, n+1) = 1 | 2019/09/15 17:00:00 | 1 | Coq 8.11.1 | Public | |

15 | Identity permutation | 2019/09/08 20:00:00 | 3 | Coq 8.11.1 | Public | |

14 | Multiplication in F_2 is idempotent | 2019/09/08 20:00:00 | 2 | Coq 8.11.1 | Public | |

13 | Definitions of injectivity | 2019/09/08 20:00:00 | 2 | Coq 8.11.1 | Public | |

12 | Summand of one | 2019/09/08 20:00:00 | 1 | Coq 8.11.1 | Public | |

11 | l1 <> l2 if l2 is an odd permutation of l1 | 2019/08/25 21:00:00 | 4 | Coq 8.11.1 | Public | |

10 | Cumulative sum of list | 2019/08/25 21:00:00 | 2 | Coq 8.11.1 | Public | |

9 | forall l: list nat, l @ [0] <> [] | 2019/08/25 21:00:00 | 1 | Coq 8.11.1 | Public | |

8 | Equivalent two quicksorts | 2019/08/18 16:00:00 | 4 | Coq 8.11.1 | Public | |

7 | Product of n consecutive integers is divisible by n! | 2019/08/18 16:00:00 | 3 | Coq 8.11.1 | Public | |

6 | n < m \/ n = m \/ n > m | 2019/08/18 16:00:00 | 2 | Coq 8.11.1 | Public | |

5 | n * S m = n + n * m | 2019/08/18 16:00:00 | 1 | Coq 8.11.1 | Public | |

4 | forall f: bool -> bool, f^3(x) = f(x) | 2019/08/18 16:00:00 | 1 | Coq 8.11.1 | Public | |

3 | 1 + 1 = 2 | 2019/08/18 16:00:00 | 1 | Coq 8.11.1 | Public | |

2 | plus_comm | 2019/08/03 09:00:00 | 1 | Coq 8.11.1 | Public | |

1 | plus_assoc | 2019/08/03 09:00:00 | 1 | Coq 8.11.1 | Public |