Fix typechecking

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}