fact: Definition is_cipher_of f a := l+1 < q /\ (forall i, i < l -> f i < power q 2) /\ a = ∑ l (fun i => f i * power (power (S i) 2) r).
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)