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