proposition: Lemma Npower_le_compat_r : forall n p q, n > 0 -> p <= q -> n ^ p <= n ^ q.
proof: Proof. intros. apply Nle_plus in H0. destruct H0. generalize x q H H0. clear H H0. clear x q. induction x. intros. rewrite Nat.add_0_r in H0. rewrite H0. auto. intros. rewrite <- Nat.add_succ_comm in H0. simpl in H0. rewrite H0. rewrite Npower_succ. replace (n^p) with (1*n^p). apply Nat.mul_le_mono. auto. apply IHx. auto. auto. ring. Qed.
imports: Arith Ntools Nle