diff options
Diffstat (limited to 'theories/Zarith/Zmisc.v')
| -rw-r--r-- | theories/Zarith/Zmisc.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v index 2aa69092ad..bc90b06123 100644 --- a/theories/Zarith/Zmisc.v +++ b/theories/Zarith/Zmisc.v @@ -303,8 +303,8 @@ Lemma Z_modulo_2 : (x:Z) `x >= 0` -> { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }. Proof. Intros x Hx. Elim (Zeven_odd_dec x); Intro. -Left. Split with (Zdiv2 x). Exact (Zeven_div2 x y). -Right. Split with (Zdiv2 x). Exact (Zodd_div2 x Hx y). +Left. Split with (Zdiv2 x). Exact (Zeven_div2 x a). +Right. Split with (Zdiv2 x). Exact (Zodd_div2 x Hx b). Save. (* Very simple *) |