next up previous contents
Next: List Up: The Natural Numbers Previous: Division

Exponentiation

 ** Module lib_nat_exp_thms Imports lib_nat_times_thms
  exp_one = ... : {n:nat}Eq (exp n one) n



Lego
1998-06-15