proposition: Lemma pow_succ_r n m : 0<=m -> n^(succ m) = n * n^m.
proof: Proof. destruct m as [|m|m]; (now destruct 1) || (intros _); simpl; trivial. unfold pow_pos. now rewrite Pos.add_comm, Pos.iter_add. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass