proposition: Lemma shiftl_spec_high a n m : 0<=m -> n<=m -> testbit (shiftl a n) m = testbit a (m-n).
proof: Proof. intros _ H. rewrite <- (sub_add n m H) at 1. set (m' := m-n). clearbody m'. clear H m. revert a m'. induction n using peano_ind; intros a m. - rewrite add_0_r; now destruct a. - rewrite shiftl_succ_r. rewrite add_comm, add_succ_l, add_comm. now rewrite testbit_succ_r_div2, div2_double by apply le_0_l. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties