Merge remote-tracking branch 'origin/pr/193'

1 files changed, 0 insertions, 12 deletions

diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 4533103..cfe0fa3 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -1596,15 +1596,3 @@ Ltac nat_congr := first
      apply: (congr1 (addn X1) _);
      symmetry
    end ].
-
-Module mc_1_6.
-
-CoInductive compare_nat m n : bool -> bool -> bool -> Set :=
-  | CompareNatLt of m < n : compare_nat m n true false false
-  | CompareNatGt of m > n : compare_nat m n false true false
-  | CompareNatEq of m = n : compare_nat m n false false true.
-
-Lemma ltngtP m n : compare_nat m n (m < n) (n < m) (m == n).
-Proof. by case: ltngtP; constructor. Qed.
-
-End mc_1_6.