Theorem: size_next_eq_size_of_no_carry (Fl/Trunc.lean)

State before:
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) = Nat.size x
Tactic:
apply Nat.le_antisymm
State after:
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x

case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)

State before:
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x

case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Tactic:
. rwa [Nat.size_le]
State after:
case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)

State before:
case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Tactic:
. exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
no goals

State before:
case h₁
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size (next n x) ≤ Nat.size x
Tactic:
rwa [Nat.size_le]
State after:
no goals

State before:
case h₂
n x : ℕ
no_carry : next n x < 2 ^ Nat.size x
⊢ Nat.size x ≤ Nat.size (next n x)
Tactic:
exact Nat.size_le_size (Nat.le_add_right _ _)
State after:
no goals