Added proof blt_nat_false.
Added proofs for dealing with max_nat.