proposition: Lemma bits_iff_neg : forall a n, log2 (abs a) < n -> (a<0 <-> a.[n] = true).
proof: Proof. intros a n Hn. now rewrite lt_nge, <- not_false_iff_true, (bits_iff_nonneg a n). Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog