proposition: Lemma mkpow_ok p x : mkpow x p == x^p.
proof: Proof. destruct p;simpl;intros;Esimpl. - rewrite !mkmult_pow_ok;Esimpl. - rewrite mkmult_pow_ok;Esimpl. change x with (x^1) at 1. now rewrite <- pow_pos_add, Pos.add_1_r, Pos.succ_pred_double. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory