Working toward proving _+_'s commutativity.
Added a 'flip' transitivity theorem in Equality. And I created a
'NaturalProperties.agda' file to contain natural-number-related proofs.