DEFINITION le_minus_plus()
TYPE =
∀z:nat
.∀x:nat
.le z x
→∀y:nat.(eq nat (minus (plus x y) z) (plus (minus x z) y))
BODY =
assume z: nat
we proceed by induction on z to prove
∀x:nat
.le z x
→∀y:nat.(eq nat (minus (plus x y) z) (plus (minus x z) y))
case O : ⇒
the thesis becomes
∀x:nat
.le O x
→∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
assume x: nat
suppose H: le O x
(H0)
by cases on H we prove
eq nat x x
→∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
case le_n ⇒
the thesis becomes
eq nat O x
→∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
suppose H0: eq nat O x
we proceed by induction on H0 to prove ∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
case refl_equal : ⇒
the thesis becomes ∀y:nat.(eq nat (minus (plus O y) O) (plus (minus O O) y))
assume y: nat
by (minus_n_O .)
we proved eq nat (plus O y) (minus (plus O y) O)
that is equivalent to eq nat (plus (minus O O) y) (minus (plus O y) O)
by (sym_eq . . . previous)
we proved eq nat (minus (plus O y) O) (plus (minus O O) y)
∀y:nat.(eq nat (minus (plus O y) O) (plus (minus O O) y))
we proved ∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
eq nat O x
→∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
case le_S m:nat H0:le O m ⇒
the thesis becomes
∀H1:eq nat (S m) x
.∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
suppose H1: eq nat (S m) x
suppose : le O m
assume y: nat
by (refl_equal . .)
we proved eq nat (plus (minus (S m) O) y) (plus (minus (S m) O) y)
that is equivalent to eq nat (minus (plus (S m) y) O) (plus (minus (S m) O) y)
le O m
→∀y:nat
.eq nat (minus (plus (S m) y) O) (plus (minus (S m) O) y)
by (previous H1 H0)
we proved ∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
∀H1:eq nat (S m) x
.∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
eq nat x x
→∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
end of H0
by (refl_equal . .)
we proved eq nat x x
by (H0 previous)
we proved ∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
∀x:nat
.le O x
→∀y:nat.(eq nat (minus (plus x y) O) (plus (minus x O) y))
case S : z0:nat ⇒
the thesis becomes
∀x:nat
.le (S z0) x
→∀y:nat.(eq nat (minus (plus x y) (S z0)) (plus (minus x (S z0)) y))
(H) by induction hypothesis we know
∀x:nat
.le z0 x
→∀y:nat.(eq nat (minus (plus x y) z0) (plus (minus x z0) y))
assume x: nat
we proceed by induction on x to prove
le (S z0) x
→∀y:nat.(eq nat (minus (plus x y) (S z0)) (plus (minus x (S z0)) y))
case O : ⇒
the thesis becomes
le (S z0) O
→∀y:nat.(eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))
suppose H0: le (S z0) O
assume y: nat
(H1)
by cases on H0 we prove
eq nat O O
→eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
case le_n ⇒
the thesis becomes
eq nat (S z0) O
→eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
suppose H1: eq nat (S z0) 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 z0 OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S z0 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 eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
we proved eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
eq nat (S z0) O
→eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
case le_S m:nat H1:le (S z0) m ⇒
the thesis becomes
∀H2:eq nat (S m) O
.eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
suppose H2: eq nat (S m) 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 m OF O⇒False | S ⇒True
consider I
we proved True
<λ:nat.Prop> CASE S m 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 z0) m
→eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
we proved
le (S z0) m
→eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
by (previous H1)
we proved eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
∀H2:eq nat (S m) O
.eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
eq nat O O
→eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
end of H1
by (refl_equal . .)
we proved eq nat O O
by (H1 previous)
we proved eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)
le (S z0) O
→∀y:nat.(eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))
case S : n:nat ⇒
the thesis becomes
∀H1:le (S z0) (S n)
.∀y:nat.(eq nat (minus (plus n y) z0) (plus (minus n z0) y))
() by induction hypothesis we know
le (S z0) n
→∀y:nat.(eq nat (minus (plus n y) (S z0)) (plus (minus n (S z0)) y))
suppose H1: le (S z0) (S n)
assume y: nat
by (le_S_n . . H1)
we proved le z0 n
by (H . previous .)
we proved eq nat (minus (plus n y) z0) (plus (minus n z0) y)
that is equivalent to
eq
nat
minus (plus (S n) y) (S z0)
plus (minus (S n) (S z0)) y
∀H1:le (S z0) (S n)
.∀y:nat.(eq nat (minus (plus n y) z0) (plus (minus n z0) y))
we proved
le (S z0) x
→∀y:nat.(eq nat (minus (plus x y) (S z0)) (plus (minus x (S z0)) y))
∀x:nat
.le (S z0) x
→∀y:nat.(eq nat (minus (plus x y) (S z0)) (plus (minus x (S z0)) y))
we proved
∀x:nat
.le z x
→∀y:nat.(eq nat (minus (plus x y) z) (plus (minus x z) y))
we proved
∀z:nat
.∀x:nat
.le z x
→∀y:nat.(eq nat (minus (plus x y) z) (plus (minus x z) y))