proposition: Lemma exp_quoV r p q : 0 <= r -> exp_quo r^-1 p q = (exp_quo r p q)^-1.
proof: Proof. rewrite /exp_quo fmorphV /=; case: q => [|q] r_ge_0. by rewrite !root0C expr0n; case: eqP; rewrite (invr0, invr1). by rewrite rootCV ?ler0q // exprVn. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith