From 80e548a878f68c748c4bc1caeba69ea4c4dffb87 Mon Sep 17 00:00:00 2001
From: valis <valery.isaev@gmail.com>
Date: Mon, 24 Jun 2024 10:29:51 +0300
Subject: [PATCH] Fix typechecking

---
 src/Algebra/Field/Algebraic.ard | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Field/Algebraic.ard b/src/Algebra/Field/Algebraic.ard
index 5be59a3b..89e4a98e 100644
--- a/src/Algebra/Field/Algebraic.ard
+++ b/src/Algebra/Field/Algebraic.ard
@@ -133,7 +133,7 @@
                         {d : Nat} (pd : \Pi (j : Fin pl.len) -> permSet-length (pl j) < d) (a : Array R n) (pl/=0 : pl.len /= 0) {p : MPoly (Fin n) R} (pp : p = BigSum \lam j => msMonomial (pc j) (pl j))
         : ∃ (m : Nat) (degree<= (change-vars p d a) m) (Inv (polyCoef (change-vars p d a) m)) \elim pp
         | idp =>
-          \let | pow>0 {n} : 0 < pow d n => NatSemiring.pow>0 $ zero<=_ <-transitive-right pd (transport Fin (suc_pred pl/=0) 0)
+          \let | pow>0 {n} : 0 < pow d n => NatSemiring.pow>0 $ zero<=_ <∘r pd (transport Fin (suc_pred pl/=0) 0)
                | (m,rd,ri) => poly-degrees {_} {\lam j => change-vars (msMonomial 1 (pl j)) d a} pc
                     (\lam j => permSet-univ {_} {AbMonoid.toCMonoid NatSemiring} (later \lam i => pow d i) (pl j))
                     (\lam j => rewrite (change-vars_monomial {_} {_} {pl j}) $ permSet-univ_monic {_} {\lam j => padd pzero (a j) + pow (padd 1 0) (pow d j)} {\lam j => pow d j}