English
For cf,cg, the encodings of cf and cg are strictly smaller than the encoding of their pair.
Русский
Для cf,cg код cf и cg меньше кодирования их пары.
LaTeX
$$$\\operatorname{encodeCode}(cf) < \\operatorname{encodeCode}(\\mathrm{pair}(cf,cg)) \\land \\operatorname{encodeCode}(cg) < \\operatorname{encodeCode}(\\mathrm{pair}(cf,cg))$$$
Lean4
theorem encode_lt_pair (cf cg) : encode cf < encode (pair cf cg) ∧ encode cg < encode (pair cf cg) :=
by
simp only [encodeCode_eq, encodeCode]
have := Nat.mul_le_mul_right (Nat.pair cf.encodeCode cg.encodeCode) (by decide : 1 ≤ 2 * 2)
rw [one_mul, mul_assoc] at this
have := lt_of_le_of_lt this (lt_add_of_pos_right _ (by decide : 0 < 4))
exact ⟨lt_of_le_of_lt (Nat.left_le_pair _ _) this, lt_of_le_of_lt (Nat.right_le_pair _ _) this⟩
