DEFINITION le_false()
TYPE =
∀m:nat.∀n:nat.∀P:Prop.(le m n)→(le (S n) m)→P
BODY =
assume m: nat
we proceed by induction on m to prove ∀n0:nat.∀P:Prop.(le m n0)→(le (S n0) m)→P
case O : ⇒
the thesis becomes ∀n:nat.∀P:Prop.(le O n)→(le (S n) O)→P
assume n: nat
assume P: Prop
suppose : le O n
suppose H0: le (S n) O
(H1)
by cases on H0 we prove (eq nat O O)→P
case le_n ⇒
the thesis becomes (eq nat (S n) O)→P
suppose H1: eq nat (S n) O
(H2)
we proceed by induction on H1 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H2
consider H2
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
(eq nat (S n) O)→P
case le_S m0:nat H1:le (S n) m0 ⇒
the thesis becomes ∀H2:(eq nat (S m0) O).P
suppose H2: eq nat (S m0) O
(H3)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S m0 OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S m0 OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H3
consider H3
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove (le (S n) m0)→P
we proved (le (S n) m0)→P
by (previous H1)
we proved P
∀H2:(eq nat (S m0) O).P
(eq nat O O)→P
end of H1
by (refl_equal . .)
we proved eq nat O O
by (H1 previous)
we proved P
∀n:nat.∀P:Prop.(le O n)→(le (S n) O)→P
case S : n:nat ⇒
the thesis becomes ∀n0:nat.∀P:Prop.(le (S n) n0)→(le (S n0) (S n))→P
(H) by induction hypothesis we know ∀n0:nat.∀P:Prop.(le n n0)→(le (S n0) n)→P
assume n0: nat
we proceed by induction on n0 to prove ∀P:Prop.(le (S n) n0)→(le (S n0) (S n))→P
case O : ⇒
the thesis becomes ∀P:Prop.(le (S n) O)→(le (S O) (S n))→P
assume P: Prop
suppose H0: le (S n) O
suppose : le (S O) (S n)
(H2)
by cases on H0 we prove (eq nat O O)→P
case le_n ⇒
the thesis becomes (eq nat (S n) O)→P
suppose H2: eq nat (S n) O
(H3)
we proceed by induction on H2 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S n OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H3
consider H3
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove P
we proved P
(eq nat (S n) O)→P
case le_S m0:nat H2:le (S n) m0 ⇒
the thesis becomes ∀H3:(eq nat (S m0) O).P
suppose H3: eq nat (S m0) O
(H4)
we proceed by induction on H3 to prove <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
case refl_equal : ⇒
the thesis becomes <λ:nat.Prop> CASE S m0 OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S m0 OF O⇒False | S ⇒True
<λ:nat.Prop> CASE O OF O⇒False | S ⇒True
end of H4
consider H4
we proved <λ:nat.Prop> CASE O OF O⇒False | S ⇒True
that is equivalent to False
we proceed by induction on the previous result to prove (le (S n) m0)→P
we proved (le (S n) m0)→P
by (previous H2)
we proved P
∀H3:(eq nat (S m0) O).P
(eq nat O O)→P
end of H2
by (refl_equal . .)
we proved eq nat O O
by (H2 previous)
we proved P
∀P:Prop.(le (S n) O)→(le (S O) (S n))→P
case S : n1:nat ⇒
the thesis becomes ∀P:Prop.∀H1:(le (S n) (S n1)).∀H2:(le (S (S n1)) (S n)).P
() by induction hypothesis we know ∀P:Prop.(le (S n) n1)→(le (S n1) (S n))→P
assume P: Prop
suppose H1: le (S n) (S n1)
suppose H2: le (S (S n1)) (S n)
(h1) by (le_S_n . . H1) we proved le n n1
(h2)
by (le_S_n . . H2)
le (S n1) n
end of h2
by (H . . h1 h2)
we proved P
∀P:Prop.∀H1:(le (S n) (S n1)).∀H2:(le (S (S n1)) (S n)).P
we proved ∀P:Prop.(le (S n) n0)→(le (S n0) (S n))→P
∀n0:nat.∀P:Prop.(le (S n) n0)→(le (S n0) (S n))→P
we proved ∀n0:nat.∀P:Prop.(le m n0)→(le (S n0) m)→P
we proved ∀m:nat.∀n0:nat.∀P:Prop.(le m n0)→(le (S n0) m)→P