def gcd_all_greatest
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/proof.bend as Proofimport Base
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-math@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))
Uses (7)
Used by (0)
No other definition uses this definition.