def ud.dq

bend-osdev-u32@0.1.0.0 · PROOF.bend:1791

import Base

1791def ud.dq(G: Word(32n) & U32) -> {U32.to_nat(U32.div.fin(G)) == ud.q(32n, G) : Nat}:
1792  match G:
1793    case (q, r):
1794      {==}