def divides_left
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/proof.bend as Proofimport Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend as G
39def divides_left(+a: Nat, +b: Nat) -> S.Gcd.divides_left(a, b):
40 (G.wl(G.ws(b, a, b)), G.gcd_dvd_left(a, b))
Uses (6)
Used by (0)
No other definition uses this definition.