- apply (le_times_to_le 16) [ autobatch | ] ;
- rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
- rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
+ apply (le_times_to_le 16) [ autobatch by le_S_S,le_O_n;| ] ;
+ rewrite > (div_mod (S b) 16) in H;[2:unfold; autobatch by le_S_S,le_O_n;|]
+ rewrite > (div_mod 255 16) in H:(? ? %);[2:unfold; autobatch by le_S_S,le_O_n;|]