Theorem: size_next_eq_succ_size_of_carry (Fl/Trunc.lean)

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

case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)

State before:
case h₁
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) ≤ Nat.size x + 1

case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Tactic:
. exact size_next_le_succ_size n x
State after:
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)

State before:
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Tactic:
. rwa [Nat.add_one, Nat.succ_le, Nat.lt_size]
State after:
no goals

State before:
case h₁
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) ≤ Nat.size x + 1
Tactic:
exact size_next_le_succ_size n x
State after:
no goals

State before:
case h₂
n x : ℕ
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 ≤ Nat.size (next n x)
Tactic:
rwa [Nat.add_one, Nat.succ_le, Nat.lt_size]
State after:
no goals