proposition: Lemma expRV x (n : nat) : x != 0 -> (/ x ) ^ n = x ^- n.
proof: Proof. move=> x0; elim : n => /= [ | n IH]; first by rewrite Rinv_1. by rewrite invRM //; [rewrite IH | exact/expR_neq0]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)