law FITS0

lawful-fields@0.1.1.0 · proof_num.bend:154

import Base

154# a < q, or a = q and k <= 5, exactly when 10a + k < 10q + 6 (k a digit).
155law FITS0:
156  for +a: Nat
157  for +q: Nat
158  for +k: Nat
159  for +hk: {Nat.is_le(k, 9n) == True{} : Bool}
160  {Bool.or(Nat.is_lt(a, q), Bool.and(Nat.is_eq(a, q), Nat.is_le(k, 5n))) == Nat.is_lt(Nat.add(Nat.mul(a, 10n), k), Nat.add(Nat.mul(q, 10n), 6n)) : Bool}