title: How to destruct values of expressions?
body: <p>I'm learning Coq and try to proof next seemingly simple property.
  Basically, I need to consider all the cases for <code>eqb x y</code>,
  but my usual approach using <code>destruct</code> and <code>induction</code> tactics fails here. </p>
  
  <pre><code>Fixpoint eqb (x:nat) (y: nat) :bool :=
  match x,y with
  | 0, 0 =&gt; true
  | S xx, S yy =&gt; eqb xx yy
  | _,_ =&gt; false
  end.
  
  Definition bool_to_nat (b:bool) :nat := 
    match b with
    | true =&gt; 1
    | false =&gt; 0
    end.
  
  Theorem should_be_easy: forall x:nat, forall y : nat,
    bool_to_nat (eqb x y) + bool_to_nat (negb (eqb x y)) = 1.
    intros x y. Abort.
  </code></pre>