proposition: Lemma half_gt0 x : 0 < x -> 0 < half x.
proof: Proof. by move=> lta; rewrite mulr_gt0 // invr_gt0 ltr0n. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)