def ms_mode

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:1050

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

1050def 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}:
1051  match bit md:
1052    case False{} _:
1053      hma
1054    case True{} True{}:
1055      N.le_trans(1n, na, Nat.mul(na, nb), hma, RT.le_mul_pos(na, nb, pos_of(nb, hmb)))
1056    case True{} False{}:
1057      small_mul(na, nb, hma, hmb)