proposition: Lemma pos_pred_shiftl_high : forall p n m, n<=m -> testbit (Pos.pred_N (Pos.shiftl p n)) m = testbit (shiftl (Pos.pred_N p) n) m.
proof: Proof. intros p n; induction n as [|n IHn] using peano_ind; intros m H. - unfold shiftl. simpl. now destruct (Pos.pred_N p). - rewrite shiftl_succ_r. destruct n as [|n]. + destruct m as [|m]. * now destruct H. * now destruct p. + destruct m as [|m]. * now destruct H. * rewrite <- (succ_pos_pred m). rewrite double_spec, testbit_even_succ by apply le_0_l. rewrite <- IHn. -- rewrite testbit_succ_r_div2 by apply le_0_l. f_equal. simpl. rewrite Pos.iter_succ. now destruct (Pos.iter xO p n). -- apply succ_le_mono. now rewrite succ_pos_pred. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties