Commit 2023-08-27 01:38 6b391efa

field_simp: Use positivity as a discharger (#6312) The main reasons is that having h : 0 < denom in the context should suffice for field_simp to do its job, without the need to manually pass h.ne or similar. Quite a few have := … ≠ 0 could be dropped, and some field_simp calls no longer need explicit arguments; this is promising. This does break some proofs where field_simp was not used as a closing tactic, and it now shuffles terms around a bit different. These were fixed. Using field_simp in the middle of a proof seems rather fragile anyways. As a drive-by contribution, positivity now knows about π > 0. fixes: #4835