def bitsq_b

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/lemire.bend:474

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

474# bit * bit == bit
475def bitsq_b(+b: Nat, +h: {Nat.is_le(b, 1n) == True{} : Bool}) -> {Nat.mul(b, b) == b : Nat}:
476  match b:
477    case 0n:
478      {==}
479    case 1n:
480      {==}
481    case 2n+q:
482      Empty.absurd({Nat.mul(2n+q, 2n+q) == 2n+q : Nat}, L.false_true(h))