Some Coq proofs.
In inductive.v we define the natural numbers as an inductive set, and prove by induction that addition is commutative. We also define binary trees and demonstrate how induction works on trees.
The file root2.v is an attempt to prove the irrationality of 2.