proposition: Lemma inv_compr x y: 0 < x -> 0 < y -> (y^-1 < x) = (x^-1 < y).
proof: Proof. move=> xp yp. rewrite -(ltr_pmul2r yp) - [_ < y](ltr_pmul2l xp). by rewrite mulVf ?(gt_eqF yp) // mulfV // (gt_eqF xp). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)