proposition: Lemma log2_shiftl : forall a n, a~=0 -> log2 (a << n) == log2 a + n.
proof: Proof. intros a n Ha. rewrite shiftl_mul_pow2, add_comm by trivial. apply log2_mul_pow2. - generalize (le_0_l a); order. - apply le_0_l. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog