diff options
| -rw-r--r-- | theories/ZArith/Zorder.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 7e33fe2b4c..949a01860f 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -354,7 +354,7 @@ Qed. Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n. Proof. - induction n; simpl; intros. apply Z.le_refl. easy. + intros n; induction n; simpl; intros. apply Z.le_refl. easy. Qed. Hint Immediate Z.eq_le_incl: zarith. |