def md_init

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

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

1088def md_init(+x: Nat) -> {mode(Nat.is_le(1n, x), x) == True{} : Bool} & {mode(Nat.is_le(1n, x), 1n) == True{} : Bool}:
1089  match x:
1090    case 0n:
1091      ({==}, {==})
1092    case 1n+y:
1093      +ez = Equal.sym(Bool, Nat.is_le(0n, y), True{}, N.zero_le(y))
1094      (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, {==}))