proposition: Lemma pow2_bits_eqb : forall n m, (2^n).[m] = eqb n m.
proof: Proof. intros n m. apply eq_true_iff_eq. rewrite eqb_eq. split. - destruct (eq_decidable n m) as [H|H]. { trivial. } now rewrite (pow2_bits_false _ _ H). - intros EQ. rewrite EQ. apply pow2_bits_true. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog