proposition: Lemma mkmult_pow_ok p r x : mkmult_pow r x p == r * x^p.
proof: Proof. revert r; induction p as [p IHp|p IHp|];intros;simpl;Esimpl;rewrite !IHp;Esimpl. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory