proposition: Lemma pow_1_r p : p^1 = p.
proof: Proof. unfold pow. simpl. now rewrite mul_comm. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef