proposition: Lemma Zpower_alt_succ_r a b : 0<=b -> a^^(Z.succ b) = a * a^^b.
proof: Proof. destruct b as [|b|b]; intros Hb; simpl. - now Z.nzsimpl. - now rewrite Pos.add_1_r, Pos.iter_op_succ by apply Z.mul_assoc. - now elim Hb. Qed.
imports: BinInt