proposition: Fact swap_spec_j : swap j = i.
proof: Proof. unfold swap. destruct (eq_nat_dec j i); auto. destruct (eq_nat_dec j j); auto; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)