Introduces equal-by-logbitp, a strategy for proving that a = b by showing that their bits are equal, and computed hints that can automate the application of this strategy.
