Attention: the list was moved to
https://github.com/dypsilon/frontend-dev-bookmarks
This page is not maintained anymore, please update your bookmarks.
kino6052
/ frontendDevlopmentBookmarks.md
Created
July 5, 2022 12:30
— forked from dypsilon/frontendDevlopmentBookmarks.md
A badass list of frontend development resources I collected over time.
kino6052
/ inf-primes.v
Created
October 13, 2021 00:56
— forked from poizan42/inf-primes.v
Proof of the infinitude of primes
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.ZArith.ZArith. | |
| Require Import Coq.ZArith.Znumtheory. | |
| Require Import Coq.Sets.Ensembles. | |
| Require Import Coq.Sets.Finite_sets. | |
| Require Import Coq.PArith.BinPos. | |
| Definition Z_ens := Ensemble Z. | |
| Print Finite. | |
| Print Empty_set. | |
| Definition is_empty_set U A := forall x, ~(In U A x). |