def le_k64
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:66
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64conv.bend as F64conv
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
66def le_k64(+k: Nat) -> {Nat.is_le(64n, Nat.add(k, 64n)) == True{} : Bool}:
67 L.subst(Nat, t => {Nat.is_le(64n, t) == True{} : Bool}, Nat.add(64n, k), Nat.add(k, 64n), NA.add_comm(64n, k), N.le_add_right(64n, k))