def p_zeros_fast

bend-osdev-bytes@0.1.1.0 · PROOF.bend:558

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

558def p_zeros_fast(+n: Nat) -> {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}:
559  Equal.sym(List<&2, U32>, B.zeros.fast(n), B.zeros(n),
560    Equal.trans(List<&2, U32>, B.zeros.go(n, Nil{}), List.append(&2, U32, B.zeros(n), Nil{}), B.zeros(n), g_zerosu(n, Nil{}), app_nilu(B.zeros(n))))