proposition: Lemma mul_pow2_bits_add : forall a n m, 0<=n -> (a*2^n).[n+m] = a.[m].
proof: Proof. intros a n m Hn. revert a m. apply le_ind with (4:=Hn). - solve_proper. - intros a m. now nzsimpl. - clear n Hn. intros n Hn IH a m. nzsimpl; trivial. rewrite mul_assoc, (mul_comm _ 2), <- mul_assoc. now rewrite double_bits_succ. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog