proposition: Lemma lead_tail_coefM (p q: {poly R}): lead_tail_coef (p*q) = (lead_tail_coef p) * (lead_tail_coef q).
proof: Proof. by rewrite /lead_tail_coef -mulrACA -tail_coefM lead_coefM. 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)