proposition: Lemma lor_lnot_diag : forall a, lor a (lnot a) == -1.
proof: Proof. intros a. bitwise as m ?. rewrite lnot_spec, bits_m1; trivial. now destruct a.[m]. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog