law mod_two_eq_zero_or_one

bend-mathlib@0.8.1.0 · nat.bend:3514

import Base

3514# A remainder modulo two is zero or one.
3515law mod_two_eq_zero_or_one:
3516  for n: Nat
3517  {Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)) == True{} : Bool}