title: How can I proove 0 <= a < b -> rem a b = a in Coq?
body: <p>I'm trying to prove this lemma</p>
  <pre><code>Require Import ZArith.
  Require Import Lia.
  
  Open Scope Z_scope.
  Import Z.
  
  Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
  
  Lemma rem_pos : forall {a b : Z},
    0 &lt;= a &lt; b -&gt;
    rem a b = a.
   intros. lia.
  </code></pre>
  <p>At this point I receive <code>Tactic failure:  Cannot find witness.</code> from <code>lia</code>.</p>
  <p>Am I doing something wrong?</p>