def wr.d5

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:277

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

277def wr.d5(+x0: Nat) -> {Nat.mul(1n, x0) == x0 : Nat}:
278  %Equal.sym(Nat, Nat.mul(1n, x0), x0, UL.nat_one_mul(x0)) : {_ == x0 : Nat}
279  {==}