proposition: Lemma exp_inv_inc n u v1 : @exp n 0 (vec_change v1 u (S (vec_pos v1 u))) = qs u * exp 0 v1.
proof: Proof. enough (forall i, exp i (vec_change v1 u (S (vec_pos v1 u))) = qs (i + u) * exp i v1). eapply H. induction v1 as [ | n x v1 IHv1 ]; analyse pos u; intros. + rewrite pos2nat_fst, Nat.add_0_r; cbn; ring. + intros; rewrite pos2nat_nxt; simpl; rewrite IHv1; unfold tonat. replace (S i+pos2nat u) with (i+S (pos2nat u)) 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)