no goals
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ toNat b₀ ≤ toNat b₁
cases h with
| inl h => subst h; exact Nat.zero_le _
| inr h => subst h; cases b₀ <;> simp;
case inl
b₁ : Bool
⊢ toNat false ≤ toNat b₁
case inl
b₀ b₁ : Bool
h : b₀ = false
⊢ toNat b₀ ≤ toNat b₁
subst h
no goals
case inl
b₁ : Bool
⊢ toNat false ≤ toNat b₁
exact Nat.zero_le _
case inr
b₀ : Bool
⊢ toNat b₀ ≤ toNat true
case inr
b₀ b₁ : Bool
h : b₁ = true
⊢ toNat b₀ ≤ toNat b₁
subst h
no goals
case inr
b₀ : Bool
⊢ toNat b₀ ≤ toNat true
cases b₀ <;> simp