proposition: Lemma half_inj (x y : R) : half x = half y -> x = y.
proof: Proof. by move => eq; rewrite - (double_half x) - (double_half y) eq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)