new_specification : string list -> thm -> thm
new_specification ["c1";...;"cn"] |- ?x1...xn. t
|- t[c1,...,cn/x1,...,xn]
# DIVMOD_EXIST_0;; val it : thm = |- !m n. ?q r. if n = 0 then q = 0 /\ r = 0 else m = q * n + r /\ r < n
# let th = REWRITE_RULE[SKOLEM_THM] DIVMOD_EXIST_0;; val th : thm = |- ?q r. !m n. if n = 0 then q m n = 0 /\ r m n = 0 else m = q m n * n + r m n /\ r m n < n
# new_specification ["DIV"; "MOD"] th;;
# DIVISION_0;; val it : thm = |- !m n. if n = 0 then m DIV n = 0 /\ m MOD n = 0 else m = m DIV n * n + m MOD n /\ m MOD n < n