proposition: Lemma double_half x : half x + half x = x.
proof: Proof. by rewrite -mulrDl-mulr2n - mulr_natr -mulrA divrr ?two_unit ?mulr1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)