proposition: Theorem dio_rel_binary_le x y : 𝔻F x -> 𝔻F y -> 𝔻R (fun v => x v ≲ y v).
proof: Proof. dio by lemma (fun v => binary_le_binomial (x v) (y v)). 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)