Under Nat

0< : Under (s _)
"zero is less than any positive natural"

and

0< : Under 3
1< : Under 3
2< : Under 3
(3< not of type Under 3)
"many indices can share the same bound"