proposition: Lemma Kpower_theory : power_theory 1 kmul (eq (A:=K)) BinNat.nat_of_N pow.
proof: Proof. constructor. intros r n; case n; simpl; auto. intros p; elim p using BinPos.Pind; auto. intros p1 H. rewrite Pnat.nat_of_P_succ_morphism; rewrite pow_S. rewrite (pow_pos_succ (Eqsth K) Mkmul); auto. rewrite H; auto. exact Eth.(Kfth).(F_R).(Rmul_assoc). Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith