From 5113278451652cd400227255f3d5d528f042e89f Mon Sep 17 00:00:00 2001 From: Aleksandar Nanevski Date: Mon, 23 Sep 2024 12:06:50 +0200 Subject: [PATCH] removed some lemmas that have recently been included into mathcomp --- examples/quicksort.v | 25 ------------------------- 1 file changed, 25 deletions(-) diff --git a/examples/quicksort.v b/examples/quicksort.v index 8f88cd7..d405474 100644 --- a/examples/quicksort.v +++ b/examples/quicksort.v @@ -28,31 +28,6 @@ Local Open Scope order_scope. (* but the development is repeated here to make the files *) (* self-contained *) -Lemma perm_onC {T : finType} (S1 S2 : {set T}) (u1 u2 : {perm T}) : - perm_on S1 u1 -> - perm_on S2 u2 -> - [disjoint S1 & S2] -> - commute u1 u2. -Proof. -move=> pS1 pS2 S12; apply/permP => t; rewrite !permM. -case/boolP : (t \in S1) => tS1. -- have /[!disjoint_subset] /subsetP {}S12 := S12. - by rewrite !(out_perm pS2) //; apply: S12; rewrite // perm_closed. -case/boolP : (t \in S2) => tS2. -- have /[1!disjoint_sym] /[!disjoint_subset] /subsetP {}S12 := S12. - by rewrite !(out_perm pS1) //; apply: S12; rewrite // perm_closed. -by rewrite (out_perm pS1) // (out_perm pS2) // (out_perm pS1). -Qed. - -Lemma tperm_on {T : finType} (x y : T) : - perm_on [set x; y] (tperm x y). -Proof. -apply/subsetP => z /[!inE]; case: tpermP => [->|->|]; -by rewrite eqxx // orbT. -Qed. - -(****) - Lemma leq_choose a b : a < b -> sumbool (a.+1 == b) (a.+1 < b).