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

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.9.1 | Public | |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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