Added Nat.pow properties

[saludes]

I needed the usual properties of Nat.pow so I added into power_more.kind. I'm not aware of your naming/structuring conventions, so I put it directly into base/Nat.

Also, I needed an auxiliary lemma pow.swap to make the whole thing work, which came out awful due to my clumsiness with the Kind language; so I look forward to a better version of it (if you want to enlighten me on this)

[racs4]

Hello, sorry for the delay and thanks for your contribution.

Could you change the functions' names and separate the definitions in different files? Actually we use this pattern in Kind: the definition Foo.Bar.foobar must be inside Foo.kind or Foo/Bar.kindor Foo/Bar/foobar.kind, so Kind can find them. So what you can do is add Nat. to each definition name and place them separately in Nat/pow/<name_of_def>.kind files.

We also suggest to change Nat.pow.add to Nat.pow.add_right and Nat.pow.swap to Nat.mul.comm.swap

[saludes]

Thanks for the comments! I renamed and split the definitions into the new folder base/Nat/pow