proposition: Lemma Zpower_nat_lt_compat u n m : (1 < 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 _; apply Z.lt_le_trans with (u * 1)%Z; auto with zarith. assert (Hv: (0 < u)%Z); auto with zarith. generalize (Zpower_nat_pos _ m Hv); auto with zarith. intros [ | m]; repeat rewrite Zpower_nat_S; try rewrite Zpower_nat_0; auto with zarith. intros HH. apply Zmult_lt_compat_l; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63