proposition: Theorem Rlt_powerRZ : forall (e : R) (n m : Z), (1 < e)%R -> (n < m)%Z -> (powerRZ e n < powerRZ e m)%R.
proof: Proof. intros e n m; case n; case m; simpl in |- *; try (unfold Z.lt in |- *; intros; discriminate); auto with real. intros p p0 H' H'0; apply Rlt_pow; auto with real. apply nat_of_P_lt_Lt_compare_morphism; auto. intros p H' H'0; replace 1%R with (/ 1)%R; auto with real. intros p p0 H' H'0; apply Rlt_trans with (r2 := 1%R). replace 1%R with (/ 1)%R; auto with real. apply Rlt_pow_R1; auto with real. intros p p0 H' H'0; apply Rinv_1_lt_contravar; auto with real. apply Rlt_pow; auto with real. apply nat_of_P_lt_Lt_compare_morphism; rewrite ZC4; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz