proposition: Lemma shiftl_shiftl : forall a n m, 0<=n -> (a << n) << m == a << (n+m).
proof: Proof. intros a n p Hn. bitwise as m Hm. rewrite 2 (shiftl_spec _ _ m) by trivial. rewrite add_comm, sub_add_distr. destruct (le_gt_cases 0 (m-p)) as [H|H]. - now rewrite shiftl_spec. - rewrite 2 testbit_neg_r; trivial. apply lt_sub_0. now apply lt_le_trans with 0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog