tweak big_oh definition to use le, not lt

also prove transitivity and a simple result.