DEFINITION le_plus_r()
TYPE =
       ∀n:nat.∀m:nat.(le m (plus n m))
BODY =
        assume n: nat
        assume m: nat
          we proceed by induction on n to prove le m (plus n m)
             case O : ⇒
                the thesis becomes le m (plus O m)
                   by (le_n .)
                   we proved le m m
le m (plus O m)
             case S : n0:nat ⇒
                the thesis becomes le m (plus (S n0) m)
                (H) by induction hypothesis we know le m (plus n0 m)
                   by (le_S . . H)
                   we proved le m (S (plus n0 m))
le m (plus (S n0) m)
          we proved le m (plus n m)
       we proved ∀n:nat.∀m:nat.(le m (plus n m))