set low precedence for _,_
streamlined _-1 for better interaction with _-2 and \<_\>
added commutativity and associativity for Nat
added equational reasoning for equivalences
adjusted operator precedences