proposition: Lemma shiftl_spec_low a n m : m<n -> testbit (shiftl a n) m = false.
proof: Proof. revert a m. induction n as [|n IHn] using peano_ind; intros a m H. - elim (le_0_l m). now rewrite compare_antisym, H. - rewrite shiftl_succ_r. destruct m as [|p]. + now destruct (shiftl a n). + rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l. apply IHn. apply add_lt_mono_l with 1. rewrite 2 (add_succ_l 0). simpl. now rewrite succ_pos_pred. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties