def md_init

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

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/lib/logic.bend as L

1087def md_init(+x: Nat) -> {mode(Nat.is_le(1n, x), x) == True{} : Bool} & {mode(Nat.is_le(1n, x), 1n) == True{} : Bool}:
1088  match x:
1089    case 0n:
1090      ({==}, {==})
1091    case 1n+y:
1092      +ez = Equal.sym(Bool, Nat.is_le(0n, y), True{}, N.zero_le(y))
1093      (L.subst(Bool, t => {mode(t, 1n+y) == True{} : Bool}, True{}, Nat.is_le(0n, y), ez, N.zero_le(y)), L.subst(Bool, t => {mode(t, 1n) == True{} : Bool}, True{}, Nat.is_le(0n, y), ez, {==}))