def fstep

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:347

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

347def fstep(+y: Nat) -> {Nat.is_le(S.factorial(y), S.factorial(1n+y)) == True{} : Bool}:
348  +f = S.factorial(y)
349  +e = Equal.trans(Nat, Nat.mul(1n+y, f), Nat.mul(f, 1n+y), Nat.add(f, Nat.mul(f, y)), NA.mul_comm(1n+y, f), NA.mul_succ(f, y))
350  L.subst(Nat, z => {Nat.is_le(f, z) == True{} : Bool}, Nat.add(f, Nat.mul(f, y)), Nat.mul(1n+y, f), Equal.sym(Nat, Nat.mul(1n+y, f), Nat.add(f, Nat.mul(f, y)), e), N.le_add_right(f, Nat.mul(f, y)))