proposition: Fact le_pirr : forall x y (H1 H2 : x <= y), H1 = H2.
proof: Proof. simpl; intros n ? H1. induction H1 as [ | m H1 IH ] using le_indd; intro H2. change (le_n n) with (eq_rect _ (fun n0 => n <= n0) (le_n n) _ eq_refl). generalize (eq_refl n). pattern n at 2 4 6 10, H2. case H2; [intro E | intros m l E]. rewrite UIP_dec with (p1 := E) (p2 := eq_refl); auto. apply eq_nat_dec. contradiction (Nat.nle_succ_diag_l m); subst; auto. change (le_S n m H1) with (eq_rect _ (fun n0 => n <= n0) (le_S n m H1) _ eq_refl). generalize (eq_refl (S m)). pattern (S m) at 1 3 4 6, H2. case H2; [intro E | intros p H3 E]. contradiction (Nat.nle_succ_diag_l m); subst; auto. injection E; intro; subst. rewrite (IH H3). rewrite UIP_dec with (p1 := E) (p2 := eq_refl); auto. apply eq_nat_dec. 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)