OVERVIEW

Banach-Tarski paradox.

INSPIRATIONS

Daniel de Rauglaudre

$ coqtop -v
The Coq Proof Assistant, version 8.20.0
compiled with OCaml 4.13.1

Name		Name	Last commit message	Last commit date
Latest commit History 3,336 Commits
.depend		.depend
.gitignore		.gitignore
Banach_Tarski.v		Banach_Tarski.v
Countable.v		Countable.v
Equidecomp.v		Equidecomp.v
GroupTransf.v		GroupTransf.v
LICENSE		LICENSE
Makefile		Makefile
Matrix.v		Matrix.v
Misc.v		Misc.v
MiscReals.v		MiscReals.v
MiscTrigo.v		MiscTrigo.v
Normalize.v		Normalize.v
NotEmptyPath.v		NotEmptyPath.v
Orbit.v		Orbit.v
OrbitRepr.v		OrbitRepr.v
Partition.v		Partition.v
Pset.v		Pset.v
README.md		README.md
Reverse.v		Reverse.v
RnCountable.v		RnCountable.v
Words.v		Words.v
interface.sh		interface.sh