proposition: Lemma shiftr_shiftl_r : forall a n m, n<=m -> (a << n) >> m == a >> (m-n).
proof: Proof. intros a n m ?. rewrite !shiftr_div_pow2, shiftl_mul_pow2. rewrite <- (sub_add n m) at 1 by trivial. rewrite pow_add_r, (mul_comm (2^(m-n))). now rewrite <- div_div, div_mul by order_nz. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog