proposition: Lemma mul_pow2_bits_high : forall a n m, n<=m -> (a*2^n).[m] = a.[m-n].
proof: Proof. intros a n m ?. rewrite <- (sub_add n m) at 1 by order'. now rewrite mul_pow2_bits_add. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog