proposition: Theorem Zpower_le : forall e1 e2, (e1 <= e2)%Z -> (Zpower r e1 <= Zpower r e2)%Z.
proof: Proof. intros e1 e2 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_1_l (r ^ e1)) at 1. apply Zmult_le_compat_r. apply (Zlt_le_succ 0). apply Zpower_gt_0. now apply Zle_minus_le_0. apply Zpower_ge_0. now apply Zle_minus_le_0. clear He. destruct e1 as [|e1|e1] ; try easy. apply Zpower_ge_0. Qed.
imports: Coq(ZArith Lia Zquot)