proposition: Fact is_cipher_of_u : l+1 < q -> is_cipher_of (fun _ => 1) (∑ l (fun i => power (power (S i) 2) r)).
proof: Proof. intros H; split; auto; split. + intros; apply (@power_mono_l 1 _ 2); lia. + apply msum_ext; intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)