title: Well founded recursion in Coq
body: <p>I am trying to write a function for computing natural division in Coq and I am having some trouble defining it since it is not structural recursion.</p>
  
  <p>My code is:</p>
  
  <pre><code>Inductive N : Set :=
    | O : N
    | S : N -&gt; N.
  
  Inductive Bool : Set :=
    | True : Bool
    | False : Bool.
  
  Fixpoint sum (m :N) (n : N) : N :=
  match m with
    | O =&gt; n
    | S x =&gt; S ( sum x n)
  end.
  
  Notation "m + n" := (sum m n) (at level 50, left associativity).
  
  Fixpoint mult (m :N) (n : N) : N :=
  match m with
    | O =&gt; O
    | S x =&gt; n + (mult x n)
  end.
  
  Notation "m * n" := (mult m n) (at level 40, left associativity).
  
  Fixpoint pred (m : N) : N :=
  match m with
    | O =&gt; S O
    | S x =&gt; x
  end.
  
  Fixpoint resta (m:N) (n:N) : N :=
  match n with
    | O =&gt; m
    | S x =&gt; pred (resta m x)
  end.
  Notation "m - x" := (resta m x) (at level 50, left associativity).
  
  Fixpoint leq_nat (m : N) (n : N) : Bool :=
  match m with
    | O =&gt; True
    | S x =&gt; match n with 
      | O =&gt; False
      | S y =&gt; leq_nat x y
    end
  end.
  
  Notation "m &lt;= n" := (leq_nat m n) (at level 70).
  
  Fixpoint div (m : N) (n : N) : N :=
  match n with
    | O =&gt; O
    | S x =&gt; match m &lt;= n with
      | False =&gt; O
      | True =&gt; pred (div (m-n) n)
    end
  end.
  </code></pre>
  
  <p>As you can see, Coq does not like my function div, it says</p>
  
  <blockquote>
    <p>Error: Cannot guess decreasing argument of <code>fix</code>.</p>
  </blockquote>
  
  <p>How can I supply in Coq a termination proof for this function? I can prove that if n>O ^ n&lt;=m -> (m-n) &lt; m.</p>