Mathlib v3 is deprecated. Go to Mathlib v4

Theorem norm_num.lt_add_of_pos_helper

Modification history

2020-05-09 20:30

src/tactic/norm_num.lean

feat(tactic/norm_num): new all-lean norm_num (#2589) …

Deleted norm_num.lt_add_of_pos_helper View on Github →

2020-04-11 04:27

src/tactic/norm_num.lean

chore(*): switch to lean 3.8.0 (#2361) …

Modified norm_num.lt_add_of_pos_helper View on Github →

2017-11-01 04:36

tactic/norm_num.lean

feat(tactic/norm_num): rewrite norm_num to use simp instead of reflection

Added norm_num.lt_add_of_pos_helper View on Github →