DEFINITION lt_x_O()
TYPE =
       ∀x:nat.(lt x O)→∀P:Prop.P
BODY =
       assume x: nat
          we must prove (lt x O)→∀P:Prop.P
          or equivalently (le (S x) O)→∀P:Prop.P
           suppose H: le (S x) O
           assume P: Prop
             (H_y) 
                by (le_n_O_eq . H)
eq nat O (S x)
             end of H_y
             (H0) 
                we proceed by induction on H_y to prove <λ:nat.Prop> CASE S x OF O⇒True | S ⇒False
                   case refl_equal : ⇒
                      the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
                         consider I
                         we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S x OF O⇒True | S ⇒False
             end of H0
             consider H0
             we proved <λ:nat.Prop> CASE S x OF O⇒True | S ⇒False
             that is equivalent to False
             we proceed by induction on the previous result to prove P
             we proved P
          we proved (le (S x) O)→∀P:Prop.P
          that is equivalent to (lt x O)→∀P:Prop.P
       we proved ∀x:nat.(lt x O)→∀P:Prop.P