proposition: Fact sum_powers_bound r n f e : r <> 0 -> (forall i, i < n -> f i < r) -> (forall i j, i < j -> e i < e j) -> sum_powers r n f e < power (e n) r.
proof: Proof. intros Hr; revert f e. induction n as [ | n IHn ]; intros f e Hf He. + rewrite msum_0; apply power_ge_1; auto. + rewrite msum_plus1; auto. apply Nat.lt_le_trans with (power (S (e n)) r). 2: apply power_mono_l; try lia; apply He; auto. rewrite power_S. apply Nat.lt_le_trans with (1*power (e n) r + f n * power (e n) r). * rewrite Nat.mul_1_l; apply Nat.add_lt_le_mono; auto. * rewrite <- Nat.mul_add_distr_r; apply Nat.mul_le_mono; auto. apply Hf; auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)