proposition: Lemma dio_fun_binomial n k : 𝔻F n -> 𝔻F k -> 𝔻F (fun ν => binomial (n ν) (k ν)).
proof: Proof. dio by lemma (fun ν => is_binomial_eq (ν 0) (n ν⭳) (k ν⭳)). Defined.
imports: Arith Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums bool_nat rel_iter) Undecidability.H10.ArithLibs(luca) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_expo)