proposition: Lemma shiftl_specif_high : forall a n m, n<=m -> testbit (shiftl a n) m = testbit a (m-n).
proof: Proof. intros a n; induction n as [|n IHn]; intros m H; [ trivial | ]. - now rewrite sub_0_r. - destruct m; [ inversion H | ]. simpl; apply succ_le_mono in H. change (shiftl a (S n)) with (double (shiftl a n)). rewrite double_twice, div2_double. now apply IHn. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass