def two_mul

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqn.bend:19

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as NL

19def two_mul(+S: Nat) -> {Nat.mul(S, 2n) == Nat.add(S, S) : Nat}:
20  NL.two_mul(S)