proposition: Theorem dio_fun_nat_meet a b : 𝔻F a -> 𝔻F b -> 𝔻F (fun ν => a ν ⇣ b ν).
proof: Proof. dio by lemma (fun v => nat_meet_dio (v 0) (a v⭳) (b 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)