proposition: Fact swap_inj n m : swap n = swap m -> n = m.
proof: Proof. intros; rewrite <- (swap_involutive n), H. apply swap_involutive. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums php)