proposition: Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false.
proof: Proof. intros n m ?. rewrite <- (mul_1_l (2^n)). destruct (le_gt_cases n m). - rewrite mul_pow2_bits_high; trivial. rewrite <- (succ_pred (m-n)) by (apply sub_gt; order). now rewrite <- div2_bits, div_small, bits_0 by order'. - rewrite mul_pow2_bits_low; trivial. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog