proposition: Lemma vec_prod_div m (v : vec nat m) (u0 : nat) (p : pos m) i : vec_pos v p = S u0 -> qs (p + i) * exp i (vec_change v p u0) = exp i v.
proof: Proof. revert p i; induction v; intros p i; analyse pos p; simpl; intros H. - rewrite pos2nat_fst; subst; simpl; ring. - rewrite pos2nat_nxt; simpl. rewrite <- IHv with (1 := H). unfold tonat. replace (S (pos2nat p + i)) with (pos2nat p+S i); 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)