proposition: Lemma local_mkpow_ok r p : match p with | xI _ => rpow r (Cp_phi (Npos p)) | xO _ => rpow r (Cp_phi (Npos p)) | 1 => r end == pow_pos rmul r p.
proof: Proof. destruct p; now rewrite ?(rpow_pow_N pow_th). Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory