proposition: Theorem Zpower_lt_Zpower : forall e1 e2, (Zpower r (e1 - 1) < Zpower r e2)%Z -> (e1 <= e2)%Z.
proof: Proof. intros e1 e2 He. apply Znot_gt_le. intros H. apply Zlt_not_le with (1 := He). apply Zpower_le. clear -H ; lia. Qed.
imports: Coq(ZArith Lia Zquot)