proposition: Lemma pow_succ_r p q : p^(succ q) = p * p^q.
proof: Proof. unfold pow. now rewrite iter_succ. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef