law divstep0

lawful-words@0.1.0.0 · proof_u32.bend:667

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

667law divstep0:
668  for +q: Nat
669  for +b: Nat
670  for +r: Nat
671  for +h: Nat
672  for +a0: Bool
673  for +s: Nat
674  for +e1: {Nat.add(Nat.mul(q, b), r) == h : Nat}
675  for +e: {s == Nat.add(N.bn(a0), Nat.double(r)) : Nat}
676  {Nat.add(Nat.mul(Nat.double(q), b), s) == Nat.add(N.bn(a0), Nat.double(h)) : Nat}