From 3548a49db7f9ddc181a27ba0762686b2f2aee30c Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Mon, 4 May 2020 11:46:30 +0900
Subject: Remove the tuple extensions in order.v that is available in tuple.v

---
 mathcomp/ssreflect/order.v | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 38ee13d..fbe92c1 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -937,20 +937,6 @@ Reserved Notation "\max^l_ ( i 'in' A ) F"
   (at level 41, F at level 41, i, A at level 50,
            format "'[' \max^l_ ( i  'in'  A ) '/  '  F ']'").
 
-(* tuple extensions *)
-Lemma eqEtuple n (T : eqType) (t1 t2 : n.-tuple T) :
-  (t1 == t2) = [forall i, tnth t1 i == tnth t2 i].
-Proof. by apply/eqP/'forall_eqP => [->|/eq_from_tnth]. Qed.
-
-Lemma tnth_nseq n T x (i : 'I_n) : @tnth n T [tuple of nseq n x] i = x.
-Proof.
-by rewrite !(tnth_nth (tnth_default (nseq_tuple n x) i)) nth_nseq ltn_ord.
-Qed.
-
-Lemma tnthS n T x (t : n.-tuple T) i :
-   tnth [tuple of x :: t] (lift ord0 i) = tnth t i.
-Proof. by rewrite (tnth_nth (tnth_default t i)). Qed.
-
 Module Order.
 
 (**************)
-- 
cgit v1.2.3