proposition: Lemma pos_pred_shiftl_low : forall p n m, m<n -> testbit (Pos.pred_N (Pos.shiftl p n)) m = true.
proof: Proof. intros p n; induction n as [|n IHn] using peano_ind. - now intro m; destruct m. - intros m H. unfold Pos.shiftl. destruct n as [|n]; simpl in *. + destruct m. * now destruct p. * elim (Pos.nlt_1_r _ H). + rewrite Pos.iter_succ. simpl. set (u:=Pos.iter xO p n) in *; clearbody u. destruct m as [|m]. * now destruct u. * rewrite <- (IHn (Pos.pred_N m)). -- rewrite <- (testbit_odd_succ _ (Pos.pred_N m)). ++ rewrite succ_pos_pred. now destruct u. ++ apply le_0_l. -- apply succ_lt_mono. now rewrite succ_pos_pred. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties