proposition: Lemma exp_quo_1 p q : (0 < q)%N -> exp_quo 1 p q = 1.
proof: Proof. by move => Hq; rewrite /exp_quo rmorph1 rootC1 // expr1n. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith