proposition: Lemma Zpower_nat_le_compat u n m : (0 < u)%Z -> (n <= m)%nat -> (Zpower_nat u n <= Zpower_nat u m)%Z.
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; auto with zarith. intros _; change 1%Z with (1 * 1)%Z; apply Zmult_le_compat; auto with zarith. generalize (Zpower_nat_pos _ m Hu); auto with zarith. intros [ | m]; repeat rewrite Zpower_nat_S; try rewrite Zpower_nat_0; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63