proposition: Lemma Zpower_Qpower : forall (a n:Z), (0<=n)%Z -> inject_Z (a^n) == (inject_Z a)^n.
proof: Proof. intros a [|n|n] H;[reflexivity| |elim H; reflexivity]. induction n using Pos.peano_ind. - replace (a^1)%Z with a by ring. ring. - rewrite Pos2Z.inj_succ. unfold Z.succ. rewrite Zpower_exp; auto with *; try discriminate. rewrite Qpower_plus' by discriminate. rewrite <- IHn by discriminate. replace (a^Zpos n*a^1)%Z with (a^Zpos n*a)%Z by ring. ring_simplify. reflexivity. Qed.
imports: Zpow_facts Qfield Qreduction