proposition: Lemma is_cipher_of_equiv f1 f2 a b : is_cipher_of f1 a -> is_cipher_of f2 b -> a = b <-> forall i, i < l -> f1 i = f2 i.
proof: Proof. intros Ha Hb; split. + intro; subst; revert Ha Hb; apply is_cipher_of_inj. + intro; revert Ha Hb; apply is_cipher_of_fun; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)