proposition: Lemma pow2_bits_true : forall n, (2^n).[n] = true.
proof: Proof. intros n. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2. now rewrite mul_pow2_bits_add, bit0_odd, odd_1. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog