proposition: Lemma exp_quo_less r1 r2 p q : (0 < q)%N -> 0 <= r1 -> 0 <= r2 -> r1 <= r2 -> exp_quo r1 p q <= exp_quo r2 p q.
proof: Proof. move => Hq H1 H2 Hleq. by rewrite exp_quo_lessE // lerXn2r ?ler_rat // nnegrE ler0q. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith