[GOAL]
b : Bool
⊢ (b::zero b) = zero b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ (false::zero false) = zero false
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ (true::zero true) = zero true
[PROOFSTEP]
rfl
[GOAL]
b : Bool
⊢ (b::zero (decide ¬b = true)) = nz (msb b)
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ (false::zero (decide ¬false = true)) = nz (msb false)
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ (true::zero (decide ¬true = true)) = nz (msb true)
[PROOFSTEP]
rfl
[GOAL]
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (nz (msb b))
[PROOFSTEP]
rw [← bit_one]
[GOAL]
C : SNum → Sort u_1
z : (b : Bool) → C (zero b)
s : (b : Bool) → (p : SNum) → C p → C (b::p)
b : Bool
⊢ C (b::zero (decide ¬b = true))
[PROOFSTEP]
exact s b (SNum.zero (Not b)) (z (Not b))
