proposition: Lemma div_pow2_bits : forall a n m, 0<=n -> 0<=m -> (a/2^n).[m] = a.[m+n].
proof: Proof. intros a n m Hn. revert a m. apply le_ind with (4:=Hn). - solve_proper. - intros a m Hm. now nzsimpl. - clear n Hn. intros n Hn IH a m Hm. nzsimpl; trivial. rewrite <- div_div by order_pos. now rewrite IH, div2_bits by order_pos. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog