proposition: Fact obtain_u_u1_value : u = ∑ l (fun i => power (power (S i) 2) r) /\ u1 = ∑ l (fun i => power (power (S (S i)) 2) r).
proof: Proof. Proof using Hu. split. + rewrite <- Hm_is_l, Hu. apply msum_ext. intros [ | i ]; simpl; auto. intros; rewrite Hk_is_power; auto; lia. + rewrite <- Hm_is_l, Hu1. apply msum_ext. intros [ | i ]; simpl; auto. * rewrite Hk_is_power; auto; lia. * intros; rewrite Hk_is_power; auto; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)