def ms_mode

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:1051

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/roots.bend as RT

1051def ms_mode(+bit: Bool, +na: Nat, +nb: Nat, +md: Bool, +hma: {mode(md, na) == True{} : Bool}, +hmb: {mode(md, nb) == True{} : Bool}) -> {mode(md, NF.msn(bit, na, nb)) == True{} : Bool}:
1052  match bit md:
1053    case False{} _:
1054      hma
1055    case True{} True{}:
1056      N.le_trans(1n, na, Nat.mul(na, nb), hma, RT.le_mul_pos(na, nb, pos_of(nb, hmb)))
1057    case True{} False{}:
1058      small_mul(na, nb, hma, hmb)