proposition: Fact swap_involutive n : swap (swap n) = n.
proof: Proof. destruct (eq_nat_dec n i). { subst n; rewrite swap_spec_i, swap_spec_j; auto. } destruct (eq_nat_dec n j). { subst n; rewrite swap_spec_j, swap_spec_i; auto. } { do 2 (rewrite swap_spec; auto). } Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)