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

Definition Npower a n := iter_nat n nat (fun _ x ⇒ a × x) 1.

Infix "^" := Npower : nat_scope.

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

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.

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.

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

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

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.

Lemma Npower_le_compat_r : ∀ n p q, n > 0 → p ≤ q → n ^ 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.