proposition: Lemma half_ltx x: 0 < x -> half x < x.
proof: Proof. by move=>lta; rewrite ltr_pdivr_mulr ?ltr0n // mulr_natr mulr2n ltr_addr. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)