diff options
Diffstat (limited to 'theories/Arith/Compare_dec.v')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 1cb91f9a5..f6801da20 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -256,7 +256,7 @@ Lemma leb_correct : forall m n, m <= n -> leb m n = true. Proof. induction m as [| m IHm]. trivial. destruct n. intro H. elim (le_Sn_O _ H). - intros. simpl in |- *. apply IHm. apply le_S_n. assumption. + intros. simpl. apply IHm. apply le_S_n. assumption. Qed. Lemma leb_complete : forall m n, leb m n = true -> m <= n. |