Theorem gt_imp_gt_of_le_of_le

Modification history

2026-06-07 02:12
Mathlib/Order/Basic.lean
feat(GRewrite): new `grw` implementation (#38318) …
Added gt_imp_gt_of_le_of_leView on Github →