INDUCTIVE DEFINITION le () [ :nat ]
OF ARITY nat→Prop
BUILT FROM:
     le_n: le n n
   | le_S: ∀m:nat.(le n m)→(le n (S m))