Systematized Natural.agda a bit more; added more arithmetic operators.
Will add proofs soon of basic arithmetic facts.