proposition: Lemma ieexprIn x : 0 < x -> x != 1 -> injective (GRing.exp x).
proof: Proof. move=> x_gt0 x_neq1 m n; without loss /subnK <-: m n / (n <= m)%N. by move=> IH eq_xmn; case/orP: (leq_total m n) => /IH->. case: {m}(m - n)%N => // m /eqP/idPn[]; rewrite -[x ^+ n]mul1r exprD. by rewrite (inj_eq (mulIf _)) ?ieexprn_weq1 ?ltW // expf_neq0 ?gt_eqF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)