Theorem: expt_le_expt (Fl/Trunc.lean)

State before:
n x y : ℕ
h : x ≤ y
⊢ expt n x ≤ expt n y
Tactic:
unfold expt
State after:
n x y : ℕ
h : x ≤ y
⊢ Nat.size x - n ≤ Nat.size y - n

State before:
n x y : ℕ
h : x ≤ y
⊢ Nat.size x - n ≤ Nat.size y - n
Tactic:
exact tsub_le_tsub_right (Nat.size_le_size h) n
State after:
no goals