Verified fixed-word core

Single-word bit, shift, and restoring-root facts are in Core.Proof.Word; nearest-even shift and quotient refinement is in Core.Proof.Rounding. Two-word representation and exact wide multiplication facts are in Core.Proof.UInt128.