diff options
| -rw-r--r-- | theories/Arith/Compare_dec.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 341dd7de5d..1afc49b7ff 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -21,7 +21,7 @@ Defined. Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n in m |- *; destruct m; auto with arith. + induction n as [|n IHn] in m |- *; destruct m as [|m]; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. @@ -33,9 +33,9 @@ Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n in m |- *. + induction n as [|n IHn] in m |- *. - left; auto with arith. - - destruct m. + - destruct m as [|m]. + right; auto with arith. + elim (IHn m); [left|right]; auto with arith. Defined. |