From 0ac34538ecfe84f2c667e053c4ddd47facac94c6 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Tue, 16 Feb 2021 13:47:28 +0300
Subject: [PATCH] A function from `Not (x = y)` to `decEq x y = No _` was
 added.

---
 libs/base/Decidable/Equality/Core.idr | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/libs/base/Decidable/Equality/Core.idr b/libs/base/Decidable/Equality/Core.idr
index 7bf75ef76..c7b49f955 100644
--- a/libs/base/Decidable/Equality/Core.idr
+++ b/libs/base/Decidable/Equality/Core.idr
@@ -27,3 +27,10 @@ decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
 decEqSelfIsYes {x} with (decEq x x)
   decEqSelfIsYes {x} | Yes Refl = Refl
   decEqSelfIsYes {x} | No contra = absurd $ contra Refl
+
+||| If you have a proof of inequality, you're sure that `decEq` would give a `No`.
+export
+decEqContraIsNo : DecEq a => {x, y : a} -> Not (x = y) -> (p ** decEq x y = No p)
+decEqContraIsNo uxy with (decEq x y)
+  decEqContraIsNo uxy | Yes xy = absurd $ uxy xy
+  decEqContraIsNo _   | No uxy = (uxy ** Refl)