proposition: Lemma Mobius0 : Mobius deg a b (0 : {poly R}) = 0.
proof: Proof. by rewrite /Mobius /shift_poly linear0 /scaleX_poly !linear0 recip0 linear0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc