mathlib documentation

tactic.omega.prove_unsats

meta def omega.prove_neg  :

Return expr of proof that given int is negative

theorem omega.forall_mem_repeat_zero_eq_zero (m : ) (x : ) (H : x list.repeat 0 m) :
x = 0

Return expr of proof that elements of (repeat 0 is.length) are all 0

Return expr of proof that the combination of linear constraints represented by ks and ts is unsatisfiable

Given a (([],les) : clause), return the expr of a term (t : clause.unsat ([],les)).

Given a (c : clause), return the expr of a term (t : clause.unsat c)

Given a (cs : list clause), return the expr of a term (t : clauses.unsat cs)