cf cg : Code
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
cf cg : Code
⊢ encode cf < encode (pair cf cg) ∧ encode cg < encode (pair cf cg)
simp [encodeCode_eq, encodeCode]
cf cg : Code
this : 1 * Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * 2 * Nat.pair (encodeCode cf) (encodeCode cg)
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
cf cg : Code
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
have := Nat.mul_le_mul_right (Nat.pair cf.encodeCode cg.encodeCode) (by decide : 1 ≤ 2 * 2)
cf cg : Code
this : Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg))
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
cf cg : Code
this : 1 * Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * 2 * Nat.pair (encodeCode cf) (encodeCode cg)
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
rw [one_mul, mul_assoc] at this
cf cg : Code
this✝ : Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg))
this : Nat.pair (encodeCode cf) (encodeCode cg) < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
cf cg : Code
this : Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg))
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
have := lt_of_le_of_lt this (lt_add_of_pos_right _ (by decide : 0 < 4))
no goals
cf cg : Code
this✝ : Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg))
this : Nat.pair (encodeCode cf) (encodeCode cg) < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
⊢ encodeCode cf < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4 ∧
    encodeCode cg < 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg)) + 4
exact ⟨lt_of_le_of_lt (Nat.left_le_pair _ _) this, lt_of_le_of_lt (Nat.right_le_pair _ _) this⟩
no goals
cf cg : Code
⊢ 1 ≤ 2 * 2
decide
no goals
cf cg : Code
this : Nat.pair (encodeCode cf) (encodeCode cg) ≤ 2 * (2 * Nat.pair (encodeCode cf) (encodeCode cg))
⊢ 0 < 4
decide