proposition: Lemma bits_above_log2_neg : forall a n, a < 0 -> log2 (P (-a)) < n -> a.[n] = true.
proof: Proof. intros a n Ha H. assert (Hn : 0<=n). { transitivity (log2 (P (-a))). - apply log2_nonneg. - order'. } rewrite <- (opp_involutive a), bits_opp, negb_true_iff by trivial. apply bits_above_log2; trivial. now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog