title: how ot proof 10%Z < Int.max_unsigned in Coq and the Int type from Compcert
body: <p>I want to proof a Z type value less than Int.max_unsigned.</p>
  
  <p>Lemma test: 10%Z &lt; Int.max_unsigned.
  Proof.
  ??
  How to prove the above test lemma?</p>