mathlib3 documentation

tactic.omega.prove_unsats

Return expr of proof that given int is negative

theorem omega.forall_mem_replicate_zero_eq_zero (m : ) (x : ) (H : x list.replicate m 0) :
x = 0

Return expr of proof that elements of (replicate is.length 0) 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)