proposition: Lemma vec_prod_mult m v (u : pos m) i : @exp m i (vec_change v u (1 + vec_pos v u)) = qs (u + i) * exp i v.
proof: Proof. revert i; induction v; analyse pos u; intros. + rewrite pos2nat_fst; simpl; ring. + rewrite pos2nat_nxt; simpl; rewrite IHv. unfold tonat. replace (pos2nat u+S i) with (S (pos2nat u+i)) by lia; ring. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW(utils utils_tac utils_list utils_nat gcd rel_iter prime pos vec)