proposition: Fact swap_spec n : n <> i -> n <> j -> swap n = n.
proof: Proof. unfold swap; intros. destruct (eq_nat_dec n i); try lia. destruct (eq_nat_dec n j); lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)