proposition: Fact exp_zero n i : @exp n i vec_zero = 1.
proof: Proof. revert i; induction n as [ | n IHn ]; intros i; simpl; auto. rewrite IHn; 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)