proposition: Lemma tail_coef0b p: p`_0 != 0 -> tail_coef p = p`_0.
proof: Proof. rewrite - {1} horner_coef0; apply: tail_coef0a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)