proposition: Theorem Zpower_lt : forall e1 e2, (0 <= e2)%Z -> (e1 < e2)%Z -> (Zpower r e1 < Zpower r e2)%Z.
proof: Proof. intros e1 e2 He2 He. destruct (Zle_or_lt 0 e1)%Z as [H1|H1]. replace e2 with (e2 - e1 + e1)%Z by ring. rewrite Zpower_plus with (2 := H1). rewrite Zmult_comm. rewrite <- (Zmult_1_r (r ^ e1)) at 1. apply Zmult_lt_compat2. split. now apply Zpower_gt_0. apply Z.le_refl. split. easy. apply Zpower_gt_1. clear -He ; lia. apply Zle_minus_le_0. now apply Zlt_le_weak. revert H1. clear -He2. destruct e1 ; try easy. intros _. now apply Zpower_gt_0. Qed.
imports: Coq(ZArith Lia Zquot)