proposition: Fact is_cipher_of_0 f a : l = 0 -> is_cipher_of f a <-> 1 < q /\ a = 0.
proof: Proof. intros ?; unfold is_cipher_of; subst l. rewrite msum_0; simpl. repeat (split; try tauto). intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)