proposition: Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0.
proof: Proof. intros a b H. bitwise as m ?. apply (orb_false_iff a.[m] b.[m]). now rewrite <- lor_spec, H, bits_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog