proposition: Lemma schange_cat l1 a l2: a != 0 -> schange (l1++a::l2) = (schange (l1++[::a]) + schange (a::l2)) %N.
proof: Proof. have aux: forall a b l n m, a * b >0 -> size (SIA l n a) = size (SIA l m b). move => c1 c2 l n m cp. rewrite -(add0n n) - (add0n m) !schangei_addm ! size_map. elim: l => // => u v Hrec /=. move: cp; case c1z: (c1 == 0); first by rewrite (eqP c1z) mul0r ltxx. case c2z: (c2 == 0); first by rewrite (eqP c2z) mulr0 ltxx. rewrite (mulrC u) (mulrC u). move => cp; have ->: (c1 * u < 0) = (c2 * u < 0). apply/idP/idP => h; [ rewrite mulrC in cp |];exact :(schange_simpl1 h cp). simpl; case: (c2 * u < 0) => //. by rewrite - (add0n 1%N) !schangei_addm ! size_map Hrec. rewrite /schange -cat1s catA => anz. have: has (fun z => z != 0) (l1 ++ [:: a]). by apply /hasP; exists a => //; rewrite mem_cat mem_head orbT. move /has_split_eq => [l3 [b [l4 [lv bnz al0]]]]. rewrite lv (schangei_s0n l4 bnz al0) -catA cat_cons (schangei_s0n _ bnz al0). rewrite /schange_index cat1s {3} /SIA eqxx anz /= - /SIA. have : a = last b l4 by move: (f_equal (last a) lv); rewrite !last_cat. move: (size l3).+1 => n; move: {2} (SIA l4 n b) (erefl (SIA l4 n b)) => s. clear lv l1; move: n b l4 bnz. elim: s. move => n b l4 bnz h alb; rewrite h add0n. have asb: all_ss b l4 by rewrite (schangei_reca _ n bnz) h eqxx. rewrite schangei_rec //; apply: aux; rewrite lt0r (mulf_neq0 bnz anz)/=. have: a \in b :: l4 by rewrite alb mem_last. rewrite inE; case /orP; first by move /eqP -> ; rewrite sqr_ge0. by move /(allP asb); rewrite mulrC. move => i s Hrec n b l4 bnz. move /(schangei_recc bnz) => [l1 [c [l5 [lv pa pb pc [pd pe]]]]] pf. have pg: a = last c l5 by rewrite pf lv last_cat last_cons. rewrite lv - catA cat_cons ! (schangei_recb _ _ pa pc) /=. by rewrite (Hrec (n + size l1).+1 c l5 pb pe pg) addSn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol