proposition: Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false.
proof: Proof. intros n m ?. destruct (le_gt_cases 0 n); [|now rewrite pow_neg_r, bits_0]. destruct (le_gt_cases n m). - rewrite <- (mul_1_l (2^n)), mul_pow2_bits; trivial. rewrite <- (succ_pred (m-n)), <- div2_bits. + now rewrite div_small, bits_0 by (split; order'). + rewrite <- lt_succ_r, succ_pred, lt_0_sub. order. - rewrite <- (mul_1_l (2^n)), mul_pow2_bits_low; trivial. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog