diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 635b72671..9db022515 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -22,7 +22,7 @@ Defined. Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n; destruct m; auto with arith. + induction n in m |- *; destruct m; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. @@ -34,7 +34,7 @@ Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n. + induction n in m |- *. auto with arith. destruct m. auto with arith. |