# mathlibdocumentation

core.init.meta.well_founded_tactics

theorem nat.lt_add_of_zero_lt_left (a b : ) :
0 < ba < a + b

theorem nat.zero_lt_one_add (a : ) :
0 < 1 + a

theorem nat.lt_add_right (a b c : ) :
a < ba < b + c

theorem nat.lt_add_left (a b c : ) :
a < ba < c + b

meta structure well_founded_tactics  :
Type
• rel_tac : expr
• dec_tac :

Argument for using_well_founded

The tactic rel_tac has to synthesize an element of type (has_well_founded A). The two arguments are: a local representing the function being defined by well founded recursion, and a list of recursive equations. The equations can be used to decide which well founded relation should be used.

The tactic dec_tac has to synthesize decreasing proofs.