proposition: Lemma mod_pow2_bits_high : forall a n m, 0<=n<=m -> (a mod 2^n).[m] = false.
proof: Proof. intros a n m (Hn,H). destruct (mod_pos_bound a (2^n)) as [LE LT]. { order_pos. } le_elim LE. - apply bits_above_log2; try order. apply lt_le_trans with n; trivial. apply log2_lt_pow2; trivial. - now rewrite <- LE, bits_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog