proposition: Lemma schange_deriv p (s := (schange p)) (s':= schange p^`()): (s = s' \/ s = s'.+1).
proof: Proof. rewrite /s/s'. have [-> | pnz] := (eqVneq p 0); first by rewrite deriv0; left. move: pnz; rewrite - size_poly_gt0 => pz. have eq: polyseq p = p`_0 :: behead p by move: pz; case p => q /=; case q => //. have aux: forall i, p^`()`_i = (nth 0 (behead p)) i *+ i.+1. by move => i; rewrite coef_deriv nth_behead. rewrite schange_sgr (schange_sgr p^`()). have <-: [seq Num.sg z | z <- (behead p)] = [seq Num.sg z | z <- p^`()]. have aux1: size (behead p) = size p^`() by rewrite size_deriv {2} eq. apply: (eq_from_nth (x0 :=0)); first by rewrite !size_map. move => i; rewrite size_map => iz;rewrite (nth_map 0)// (nth_map 0) -?aux1//. by rewrite coef_deriv nth_behead sgrMn mul1r. rewrite eq /= /schange/filter0/filter;case h: (Num.sg p`_0 != 0); last by left. simpl; case h': (_ < 0); [ by rewrite addSn; right | by left]. 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)