def mod_if_ok

lawful-words@0.1.0.0 · proof_u32.bend:854

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

854def mod_if_ok(+x: Word(32n), +y: Word(32n), +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {U32.is_zero(U32{y}) == z : Bool}) ->
855  {U32.to_nat(U32.mod.if(x, U32{y}, z)) == Nat.mod(Word.to_nat(32n, x), Word.to_nat(32n, y)) : Nat}:
856  match z:
857    case True{}:
858      %Equal.sym(Nat, Word.to_nat(32n, y), 0n, N.eq_sound(Word.to_nat(32n, y), 0n, %is_zero_to_nat(U32{y}) : {_ == True{} : Bool}; ez)) :
859        {Word.to_nat(32n, x) == Nat.mod(Word.to_nat(32n, x), _) : Nat}
860      {==}
861    case False{}:
862      mod_fin_ok(Word.to_nat(32n, x), Word.to_nat(32n, y), U32.divmod.go(32n, x, U32{y}),
863        dm_ok(32n, x, U32{y}, ne_zero_pos(Word.to_nat(32n, y), %is_zero_to_nat(U32{y}) : {_ == False{} : Bool}; ez), m, hm))