proposition: Lemma pow2_bits_true : forall n, 0<=n -> (2^n).[n] = true.
proof: Proof. intros n ?. rewrite <- (mul_1_l (2^n)). now rewrite mul_pow2_bits, sub_diag, bit0_odd, odd_1. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog