proposition: Lemma schange0_odd l: last 0 l != 0 -> odd (schange l + (0 < head 0 (filter0 l) * last 0 l)%R).
proof: Proof. rewrite /schange. have -> : filter0 l = [seq z <- 0::l | z != 0]. by rewrite /filter0 {2} /filter eqxx. rewrite (lastI 0 l); set b := (last 0 l) => bnz; rewrite filter_rcons bnz. set s := [seq z <- belast 0 l | z != 0]. have: all (fun z => z != 0) s by apply : filter_all. elim: s; first by rewrite /= mulr0 ltxx square_pos //. move => c s /=; set C:= changes _; set d:= head 0 _ => hr /andP [cnz etc]. have dnz: d != 0 by move: etc; rewrite /d; case s => // s' l' /= /andP []. rewrite addnC addnA addnC; move: (hr etc). rewrite -sgr_gt0 - (sgr_gt0 (c*b)) - sgr_lt0 ! sgrM. rewrite /sgr - if_neg - (if_neg (c==0))- (if_neg (b==0)) bnz dnz cnz. by case (d<0); case (b<0); case (c<0); rewrite ?mulrNN ? mulr1 ?mul1r ?ltr01 ?ltrN10 ? ltr10 ? ltr0N1 ?addn0 ? addnS ?addn0//=; move => ->. 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)