α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ decodeSum n = none
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ decode n = none
suffices decodeSum n = none by
  change (decodeSum n).bind _ = none
  rw [this]
  rfl
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ decodeSum n = none
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ decodeSum n = none
have : 1 ≤ n / 2 := by
  rw [Nat.le_div_iff_mul_le]
  exacts [h, by decide]
case intro
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ decodeSum n = none
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
⊢ decodeSum n = none
cases' exists_eq_succ_of_ne_zero (_root_.ne_of_gt this) with m e
case intro
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ (match (bodd n, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none
case intro
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ decodeSum n = none
simp [decodeSum, div2_val]
no goals
case intro
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : 1 ≤ n / 2
m : ℕ
e : n / 2 = succ m
⊢ (match (bodd n, n / 2) with
    | (false, m) => Option.map Sum.inl (decode m)
    | (fst, m) => Option.map Sum.inr (decode m)) =
    none
cases bodd n <;> simp [e]
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ Option.bind (decodeSum n) (some ∘ ↑Equiv.boolEquivPUnitSumPUnit.symm) = none
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ decode n = none
change (decodeSum n).bind _ = none
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ Option.bind none (some ∘ ↑Equiv.boolEquivPUnitSumPUnit.symm) = none
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ Option.bind (decodeSum n) (some ∘ ↑Equiv.boolEquivPUnitSumPUnit.symm) = none
rw [this]
no goals
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ Option.bind none (some ∘ ↑Equiv.boolEquivPUnitSumPUnit.symm) = none
rfl
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ 0 < 2
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ 1 ≤ n / 2
rw [Nat.le_div_iff_mul_le]
no goals
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ 0 < 2
exacts [h, by decide]
no goals
α : Type ?u.18106
β : Type ?u.18109
n : ℕ
h : 2 ≤ n
⊢ 0 < 2
decide