unfold sub_left_monotonic
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ sub_left_monotonic n round ∧ sub_right_monotonic n round
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    sub_right_monotonic n round