def Gcd.mul_left

bend-collections-laws-math@1.0.0.0 · spec/math/natural.bend:144

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

144def Gcd.mul_left(+c: Nat, +a: Nat, +b: Nat) -> Type:
145  {M.gcd(Nat.mul(c, a), Nat.mul(c, b)) == Nat.mul(c, M.gcd(a, b)) : Nat}