finished a proof of natToBitsLe k (bitsToNatLe v) = Just v