def sq_mode

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

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

995def sq_mode(+more: Bool, +nb: Nat, +md: Bool, +hm: {mode(md, nb) == True{} : Bool}) -> {mode(md, NF.sqn(more, nb)) == True{} : Bool}:
996  match more md:
997    case False{} _:
998      hm
999    case True{} True{}:
1000      N.le_trans(1n, nb, Nat.mul(nb, nb), hm, RT.le_mul_pos(nb, nb, pos_of(nb, hm)))
1001    case True{} False{}:
1002      small_mul(nb, nb, hm, hm)