proposition: Lemma lnot_spec : forall a n, 0<=n -> (lnot a).[n] = negb a.[n].
proof: Proof. intros a n ?. unfold lnot. rewrite <- (opp_involutive a) at 2. rewrite bits_opp, negb_involutive; trivial. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog