proposition: Lemma shiftl_spec : forall a n m, 0<=m -> (a << n).[m] = a.[m-n].
proof: Proof. intros a n m ?. destruct (le_gt_cases n m). - now apply shiftl_spec_high. - rewrite shiftl_spec_low, testbit_neg_r; trivial. now apply lt_sub_0. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog