+ 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|]
+ lapply (le_to_le_plus_to_le ? ? ? ? ? H);
+ [apply lt_S_to_le;
+ apply lt_mod_m_m;autobatch
+ |rewrite > sym_times;
+ rewrite > sym_times in ⊢ (? ? %); (* just to speed up qed *)
+ normalize in \vdash (? ? %);apply Hletin;
+ ]