def gcd_all_greatest

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/proof.bend:68

import 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/lists.bend as LS

68def gcd_all_greatest(+d: Nat, +xs: List<&2, Nat>, +ks: List<&2, Nat>, h: S.dvd_with(d, xs, ks)) -> S.GcdAll.greatest(d, xs, ks, h):
69  (LS.gw_dvd(xs, ks, 0n, 0n), LS.dvd_gcd_all(d, xs, ks, h))