fact: Definition the_cipher f : l+1 < q -> (forall i, i < l -> f i < power q 2) -> { c | is_cipher_of f c }.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)