law div_le4

lawful-bytes@0.1.1.0 · proof_fast_find.bend:834

import Base

834law div_le4:
835  for +a: Nat
836  for +b: Nat
837  for +h: {Nat.is_le(a, b) == True{} : Bool}
838  {Nat.is_le(Nat.div(a, 4n), Nat.div(b, 4n)) == True{} : Bool}