proposition: Lemma shiftl_spec_low a n m : m<n -> testbit (shiftl a n) m = false.
proof: Proof. intros H. destruct n as [|n|n], m as [|m|m]; try easy; simpl shiftl. - destruct (Pos.succ_pred_or n) as [-> | <-]; rewrite ?Pos.iter_succ; apply testbit_even_0. - destruct a as [ |a|a]. + replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). apply testbit_0_l. + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite testbit_Zpos by easy. exact (N.shiftl_spec_low (N.pos a) (N.pos n) (N.pos m) H). + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite testbit_Zneg by easy. now rewrite (N.pos_pred_shiftl_low a (N.pos n)). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass