proposition: Lemma Zpower_nat_le_reg u n m : (1 < u)%Z -> (Zpower_nat u n <= Zpower_nat u m)%Z -> (n <= m)%nat .
proof: Proof. intros Hu; generalize m; clear m; induction n as [ | n Hrec]; auto with zarith. intros [ | m]; repeat rewrite Zpower_nat_S; try rewrite Zpower_nat_0. intros Hv; contradict Hv; apply Zlt_not_le. apply Z.lt_le_trans with (u * 1)%Z; auto with zarith. assert (HH: (0 < u)%Z); auto with zarith. assert (HH1:= Zpower_nat_pos u n HH); auto with zarith. intros Hv; assert (n <= m)%nat; auto with arith. apply Hrec; apply Zmult_le_reg_r with u; auto with zarith; repeat rewrite <- (Zmult_comm u); auto. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63