proposition: Fact dp_size_fix_comp o p q : dp_size (dp_comp o p q) = 1 + dp_size p + dp_size q.
proof: Proof. auto. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10.Dio(dio_logic dio_single) Undecidability.H10.ArithLibs(Zp lagrange)