diff --git a/src/monalg.v b/src/monalg.v
index 9ac128d..3e07e49 100644
--- a/src/monalg.v
+++ b/src/monalg.v
@@ -137,11 +137,30 @@ Local Open Scope monom_scope.
 #[export]
 HB.instance Definition _ := Monoid.isLaw.Build M 1 mmul mulmA mul1m mulm1.
 
+Definition expmn (x : M) (n : nat) : M := iterop n *%M x 1%M.
+
+Arguments expmn : simpl never.
+
 Lemma unitmP (x y : M) : reflect (x == 1 /\ y == 1) (x * y == 1).
 Proof.
 by apply: (iffP eqP)=> [/unitm[-> ->]|[/eqP-> /eqP->]] //; rewrite mulm1.
 Qed.
 
+Lemma mulm_eq1 (x y : M) : (x * y == 1) = (x == 1) && (y == 1).
+Proof. exact/unitmP/andP. Qed.
+
+Lemma expmnS (x : M) (n : nat) : expmn x n.+1 = x * expmn x n.
+Proof. by rewrite /expmn !Monoid.iteropE iterS. Qed.
+
+Lemma expmnD (x : M) (n m : nat) : expmn x (n + m) = expmn x n * expmn x m.
+Proof.
+elim: n => [|n IHn]; first by rewrite mul1m.
+by rewrite addSn !expmnS IHn mulmA.
+Qed.
+
+Lemma expmnSr (x : M) (n : nat) : expmn x n.+1 = expmn x n * x.
+Proof. by rewrite -addn1 expmnD. Qed.
+
 End Monomial.
 
 #[export]
@@ -1414,8 +1433,6 @@ Definition mulcm m1 m2 : cmonom I :=
 
 Definition divcm m1 m2 : cmonom I := [cmonom m1 i - m2 i | i in finsupp m1]%M.
 
-Definition expcmn m n : cmonom I := iterop n mulcm m onecm.
-
 Lemma onecmE i : onecm i = 0%N.
 Proof. by rewrite fsfun_ffun insubF. Qed.
 
@@ -1454,6 +1471,9 @@ HB.instance Definition _ := Choice_isMonomialDef.Build (cmonom I)
   mulcmA mul0cm mulcm0 mulcm_eq0.
 HB.instance Definition _ := MonomialDef_isConomialDef.Build (cmonom I) mulcmC.
 
+#[deprecated(since="multinomials 2.5.0", use=expmn)]
+Definition expcmn m n : cmonom I := expmn m n.
+
 End CmonomCanonicals.
 
 (* -------------------------------------------------------------------- *)
@@ -1552,8 +1572,9 @@ Qed.
 Lemma mdeg_eq0 m : (mdeg m == 0%N) = (m == 1%M).
 Proof. exact/mf_eq0. Qed.
 
+#[deprecated(since="multinomials 2.5.0", use=mulm_eq1)]
 Lemma cmM_eq1 m1 m2 : (m1 * m2 == 1)%M = (m1 == 1%M) && (m2 == 1%M).
-Proof. by rewrite -!mdeg_eq0 mdegM addn_eq0. Qed.
+Proof. exact: mulm_eq1. Qed.
 
 Lemma cm1_eq1 i : (U_(i) == 1)%M = false.
 Proof. by rewrite -mdeg_eq0 mdegU. Qed.
@@ -1761,8 +1782,9 @@ Qed.
 Lemma fdeg_eq0 m : (fdeg m == 0%N) = (m == 1%M).
 Proof. exact/mf_eq0. Qed.
 
+#[deprecated(since="multinomials 2.5.0", use=mulm_eq1)]
 Lemma fmM_eq1 m1 m2 : (m1 * m2 == 1)%M = (m1 == 1%M) && (m2 == 1%M).
-Proof. by rewrite -!fdeg_eq0 fdegM addn_eq0. Qed.
+Proof. exact: mulm_eq1. Qed.
 
 Lemma fm1_eq1 i : (U_(i) == 1)%M = false.
 Proof. by rewrite -fdeg_eq0 fdegU. Qed.