proposition: Theorem dio_rel_Code_mult l q a b c : 𝔻F l -> 𝔻F q -> 𝔻F a -> 𝔻F b -> 𝔻F c -> 𝔻R (fun v => Code_mult (l v) (q v) (a v) (b v) (c v)).
proof: Proof. intros; unfold Code_mult; dio auto. Defined.
imports: Arith List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums bool_nat) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_expo dio_binary)