def div_if_ok

lawful-words@0.1.0.0 · proof_u32.bend:843

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

843def div_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}) ->
844  {U32.to_nat(U32.div.if(x, U32{y}, z)) == Nat.div(Word.to_nat(32n, x), Word.to_nat(32n, y)) : Nat}:
845  match z:
846    case True{}:
847      %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)) :
848        {0n == Nat.div(Word.to_nat(32n, x), _) : Nat}
849      {==}
850    case False{}:
851      div_fin_ok(Word.to_nat(32n, x), Word.to_nat(32n, y), U32.divmod.go(32n, x, U32{y}),
852        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))