proposition: Theorem pow_monotone: forall n p q, (1 < n)%nat -> (p < q)%nat -> (pow n p < pow n q)%nat.
proof: Proof. intros n p1 q1 H H1; elim H1; simpl. pattern (pow n p1) at 1; rewrite <- (Nat.mul_1_l (pow n p1)). apply Nat.mul_lt_mono_pos_r; auto. apply pow_pos; auto with arith. intros n1 H2 H3. apply Nat.lt_trans with (1 := H3). pattern (pow n n1) at 1; rewrite <- (Nat.mul_1_l (pow n n1)). apply Nat.mul_lt_mono_pos_r; auto. apply pow_pos; auto with arith. Qed.
imports: Arith