diff options
Diffstat (limited to 'theories/Arith/Le.v')
| -rwxr-xr-x | theories/Arith/Le.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 7765187cf5..5321637bea 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -12,6 +12,8 @@ Import nat_scope. Open Scope nat_scope. +Implicit Variables Type m,n,p:nat. + Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)). Proof. NewInduction 1; Auto. |