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