# Library Coqtail.Arith.Npow

Require Import Arith.
Require Export Ntools.
Require Export Nle.
Open Scope nat_scope.

# Definition of power over nat

Definition using iter_nat
Definition Npower a n := iter_nat n nat (fun _ xa × x) 1.
Notation
Infix "^" := Npower : nat_scope.

# Simplification

Simplification of n ^ 1
Lemma Npower_n_1: x, x ^ 1 = x.
intros.
unfold Npower.
unfold iter_nat.
apply mult_1_r.
Qed.

Relation with successor
Lemma Npower_succ : a n, a ^ (S n) = a × a ^ n.
Proof.
intros.
unfold Npower. unfold iter_nat.
fold iter_nat. fold Npower.
reflexivity.
Qed.

Simplification of 1 ^ n
Lemma Npower_1_n : n, 1 ^ n = 1.
Proof.
induction n.
compute. reflexivity.
unfold Npower.
unfold iter_nat. fold iter_nat.
unfold Npower in IHn.
rewrite IHn.
auto with arith.
Qed.

Simplification of 0 ^ n
Lemma Npower_0_n : n, n > 1 → 0 ^ n = 0.
Proof.
destruct n.
intros.
inversion H.
intros.
compute.
auto.
Qed.

Simplification of n ^ 0
Lemma Npower_n_0 : n, n>1 → n ^ 0 = 1.
Proof.
compute. auto.
Qed.

# Compatibility with order

Lemma Npower_plus_le_compat : a b c, c > 0 → (a + b) ^ c a ^ c + b ^ c.
Proof.
induction c.
intros.
inversion H.
intros.
rewrite Npower_succ.
rewrite mult_plus_distr_r.
apply plus_le_compat.
rewrite Npower_succ.
apply mult_le_compat_l.
destruct c.
compute. auto.
apply le_trans with (a^(S c)+b^(S c)).
auto with arith.
apply IHc.
auto with arith.

rewrite Npower_succ.
apply mult_le_compat_l.
destruct c.
compute. auto.
apply le_trans with (a^(S c)+b^(S c)).
auto with arith.
apply IHc.
auto with arith.
Qed.

Compatibility and order
Lemma Npower_le_compat_r : n p q, n > 0 → p qn ^ p n ^ q.
Proof.
intros.
apply Nle_plus in H0.
destruct H0.
generalize x q H H0.
clear H H0. clear x q.
induction x.
intros.
rewrite plus_0_r in H0.
rewrite H0.
auto.

intros.
rewrite <- plus_Snm_nSm in H0.
simpl in H0.
rewrite H0.
rewrite Npower_succ.
replace (n^p) with (1×n^p).
apply mult_le_compat.
auto.
apply IHx.
auto.
auto.
ring.
Qed.