Add some IsTrunc typeclass documentation

Also, reorder Overture.v a bit so we can put all the truncation code in
one place.  Perhaps the typeclass machinery should go with tactics?
Maybe?