~/jendhub

def odd2_t1_at

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:154

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/bgcdnat.bend as Bgcdnat
import Base

154def odd2_t1_at(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +m: Nat, +d: Nat, +ka: Nat, +kb: Nat, +ea: {a == Nat.mul(ka, d) : Nat}, +eb: {Nat.double(m) == Nat.mul(kb, d) : Nat}) -> dvd2(d, a, m):
155  ((ka, ea), odd2_m(m, d, odd_dvd_r(a, ha, d, ka, ea, Nat.mod(d, 2n), {==}), kb, eb, Nat.mod(kb, 2n), {==}))

Uses (8)

Used by (1)