def two_mul

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqk.bend:43

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqn.bend as QN

43def two_mul(+x: Nat) -> {Nat.mul(x, 2n) == Nat.add(x, x) : Nat}:
44  QN.two_mul(x)