feat(Order/Basic): add gcongr lemmas

[urkud]

---

[github-actions]

PR summary 63d7ddf060

Import changes exceeding 2%

%	File
+4.42%	Mathlib.Order.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Basic	113	118	+5 (+4.42%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.ClosedUnderIsomorphisms	4
12 files Mathlib.Order.Compare Mathlib.Algebra.Order.Group.Synonym Mathlib.Order.Max Mathlib.Order.ULift Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Order.Synonym Mathlib.Order.Basic Mathlib.Data.Nat.Cast.Synonym Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.GroupWithZero.Synonym	5

---

Declarations diff

++ ⟨_,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[urkud]

Should I put these lemmas elsewhere instead?

[YaelDillies]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.