law mod_two_eq_zero_or_one_sym

bend-mathlib@0.8.1.0 · nat.bend:4768

import Base

4768# A remainder modulo two is zero or one, reversed to rewrite toward the simple side.
4769law mod_two_eq_zero_or_one_sym:
4770  for n: Nat
4771  {True{} == Bool.or(Nat.is_eq(Nat.mod(n, 2n), 0n), Nat.is_eq(Nat.mod(n, 2n), 1n)) : Bool}