diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
index 7acfab27b7..923ab4c57f 100644
--- a/CHANGELOG_NEXT.md
+++ b/CHANGELOG_NEXT.md
@@ -217,6 +217,17 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added implementations of `Foldable` and `Traversable` for `Control.Monad.Identity`
 
+* Multiple functions in `Data.Nat` and `Data.Nat.Order.Properties` (mostly inequality proofs) are now `public export`:
+  - `fromLteSucc`
+  - `lteSuccLeft`, `lteSuccRight`
+  - `lteAddRight`
+  - `divCeilNZ` (it is `total` now as well)
+  - `plusLteMonotoneLeft`, `plusLteMonotoneRight`, `plusLteMonotone`
+  - `minusPos`, `minusLteMonotone`, `minusLtMonotone`
+  - `minusLTE`, `minusPosLT`
+  - `multLteMonotoneLeft`, `multLteMonotoneRight`
+  - `decomposeLte`
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.
diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr
index 7adb885cad..b020af34a4 100644
--- a/libs/base/Data/Nat.idr
+++ b/libs/base/Data/Nat.idr
@@ -174,7 +174,7 @@ export
 succNotLTEzero : Not (LTE (S m) Z)
 succNotLTEzero LTEZero impossible
 
-export
+public export
 fromLteSucc : LTE (S m) (S n) -> LTE m n
 fromLteSucc (LTESucc x) = x
 
@@ -220,16 +220,16 @@ ltRecall : LT m n -> {p : Nat -> Nat} -> (0 prf : LT (p m) q) -> LT (p m) q
 ltRecall {m} x prf with (lteRecallLeft x)
   ltRecall {m = m} x prf | (S m ** Refl) = irrelevantLte prf
 
-export
+public export
 lteSuccRight : LTE n m -> LTE n (S m)
 lteSuccRight LTEZero     = LTEZero
 lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
 
-export
+public export
 lteSuccLeft : LTE (S n) m -> LTE n m
 lteSuccLeft (LTESucc x) = lteSuccRight x
 
-export
+public export
 lteAddRight : (n : Nat) -> LTE n (n + m)
 lteAddRight Z = LTEZero
 lteAddRight (S k) {m} = LTESucc (lteAddRight {m} k)
@@ -374,8 +374,7 @@ export partial
 divNat : Nat -> Nat -> Nat
 divNat left (S right) = divNatNZ left (S right) SIsNonZero
 
-export
-covering
+public export
 divCeilNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 divCeilNZ x y p = case (modNatNZ x y p) of
   Z   => divNatNZ x y p
@@ -516,8 +515,8 @@ plusLeftLeftRightZero left right p =
   ~~ left     ...(p)
   ~~ left + 0 ..<(plusZeroRightNeutral left)
 
-export
-plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
+public export
+plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q + p) `LTE` (r + p)
 plusLteMonotoneRight p  Z     r     LTEZero    = CalcSmart {leq = LTE} $
   |~ 0 + p
   <~ p + r ...(lteAddRight p)
@@ -527,7 +526,7 @@ plusLteMonotoneRight p (S q) (S r) (LTESucc q_lte_r) =
   |~ q + p
   <~ r + p ...(plusLteMonotoneRight p q r q_lte_r)
 
-export
+public export
 plusLteMonotoneLeft : (p, q, r : Nat) -> q `LTE` r -> (p + q) `LTE` (p + r)
 plusLteMonotoneLeft p q r q_lt_r = CalcSmart {leq = LTE} $
   |~ p + q
@@ -536,7 +535,7 @@ plusLteMonotoneLeft p q r q_lt_r = CalcSmart {leq = LTE} $
   <~ p + r .=.(plusCommutative r p)
 
 
-export
+public export
 plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q ->
                   (m + p) `LTE` (n + q)
 plusLteMonotone left right = CalcSmart {leq = LTE} $
@@ -679,19 +678,19 @@ minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
 minusPlusZero Z     _ = Refl
 minusPlusZero (S n) m = minusPlusZero n m
 
-export
+public export
 minusPos : m `LT` n -> Z `LT` minus n m
 minusPos lt = case view lt of
   LTZero    => ltZero
   LTSucc lt => minusPos lt
 
-export
+public export
 minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p
 minusLteMonotone LTEZero = LTEZero
 minusLteMonotone {p = Z} prf@(LTESucc _) = prf
 minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte
 
-export
+public export
 minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
 minusLtMonotone {m} {p} mltn pltn = case view pltn of
     LTZero => ltRecall {p = (`minus` 0)} mltn $ CalcSmart {leq = LT} $
diff --git a/libs/base/Data/Nat/Order/Properties.idr b/libs/base/Data/Nat/Order/Properties.idr
index 2fe81fb526..7b102ab431 100644
--- a/libs/base/Data/Nat/Order/Properties.idr
+++ b/libs/base/Data/Nat/Order/Properties.idr
@@ -71,7 +71,7 @@ GTIsnotlte a b prf =
     succNotLTEpred $ transitive prf contra
 
 ||| Subtracting a number gives a smaller number
-export
+public export
 minusLTE : (a,b : Nat) -> (b `minus` a) `LTE` b
 minusLTE a      0    = LTEZero
 minusLTE 0     (S _) = reflexive
@@ -81,15 +81,15 @@ minusLTE (S a) (S b) =
     (lteSuccRight reflexive)
 
 ||| Subtracting a positive number gives a strictly smaller number
-export
+public export
 minusPosLT : (a,b : Nat) -> 0 `LT` a -> a `LTE` b -> (b `minus` a) `LT` b
 minusPosLT 0     b     z_lt_z           a_lte_b impossible
 minusPosLT (S a) 0     z_lt_sa          a_lte_b impossible
 minusPosLT (S a) (S b) z_lt_sa          a_lte_b = LTESucc (minusLTE a b)
 
 -- This is the opposite of the convention in `Data.Nat`, but 'monotone on the left' means the below
-export
-multLteMonotoneRight : (l, a, b : Nat) -> a `LTE` b -> l*a `LTE` l*b
+public export
+multLteMonotoneRight : (l, a, b : Nat) -> a `LTE` b -> (l * a) `LTE` (l * b)
 multLteMonotoneRight  0    a b _ = LTEZero
 multLteMonotoneRight (S k) a b a_lte_b = CalcWith {leq = LTE} $
   |~ (1 + k) * a
@@ -99,8 +99,8 @@ multLteMonotoneRight (S k) a b a_lte_b = CalcWith {leq = LTE} $
                      multLteMonotoneRight k    a     b   a_lte_b)
   ~~ (1 + k) * b ...(Refl)
 
-export
-multLteMonotoneLeft : (a, b, r : Nat) -> a `LTE` b -> a*r `LTE` b*r
+public export
+multLteMonotoneLeft : (a, b, r : Nat) -> a `LTE` b -> (a * r) `LTE` (b * r)
 multLteMonotoneLeft a b r a_lt_b =
   rewrite multCommutative a r in
   rewrite multCommutative b r in
@@ -113,7 +113,7 @@ lteNotLtEq a b a_lte_b not_n_lte_n =
   in antisymmetric a_lte_b b_lte_a
 
 -- Try succ left element LTE. Returns LT if successful, otherwise proof of equality a and b
-export
+public export
 decomposeLte : (a, b : Nat) -> LTE a b -> Either (LT a b) (a = b)
 decomposeLte a b a_lte_b with (isLT a b)
   decomposeLte a b a_lte_b | Yes a_lt_b = Left a_lt_b