proposition: Fact lt_pirr x y (H1 H2 : x < y) : H1 = H2.
proof: Proof. apply le_pirr. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)