[Add] Properties of rounding in Rational#2953

Draft

aortega0703 wants to merge 20 commits intoagda:masterfrom

aortega0703:rounding-properties

Commits on Feb 19, 2026

floor upper bound, ceil lower bound
aortega0703
committed

Commits on Feb 21, 2026

Add bounds for floor and ceil
aortega0703
committed

Commits on Feb 24, 2026

add introduction of absolute value via inequalities
aortega0703
committed

Commits on Feb 26, 2026

Commits on Feb 27, 2026

Commits on Feb 28, 2026

Commits on Mar 2, 2026

Commits on Mar 12, 2026

Merge branch 'master' of github.com:agda/agda-stdlib into rounding-properties
aortega0703
committed

Commits on Mar 18, 2026