Let's build a simple proof assistant using built-in ocaml GADTs
Fourrier is nice, but do there exist two periodic functions $f,g : \mathbb{R} \to \mathbb{R}$ such that $\forall x \in \mathbb{R},\ f(x)+g(x)=x$? Well, with the axiom of choice, that is the case! This and more.