From b7281bfec24725aa9ea262df01bd772e78dff6e0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 4 Apr 2020 15:12:15 +0200
Subject: Adding properties about implb.

This addresses a question on gitter (April 4).
---
 .../12018-master+implb-characterization.rst           | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 doc/changelog/10-standard-library/12018-master+implb-characterization.rst

(limited to 'doc')

diff --git a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst
new file mode 100644
index 0000000000..4b0abdfa3b
--- /dev/null
+++ b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst
@@ -0,0 +1,19 @@
+- **Added:**
+  Added lemmas
+  :g:`orb_negb_l`,
+  :g:`andb_negb_l`,
+  :g:`implb_true_iff`,
+  :g:`implb_false_iff`,
+  :g:`implb_true_r`,
+  :g:`implb_false_r`,
+  :g:`implb_true_l`,
+  :g:`implb_false_l`,
+  :g:`implb_same`,
+  :g:`implb_contrapositive`,
+  :g:`implb_negb`,
+  :g:`implb_curry`,
+  :g:`implb_andb_distrib_r`,
+  :g:`implb_orb_distrib_r`,
+  :g:`implb_orb_distrib_l` in library :g:`Bool`
+  (`#12018 <https://github.com/coq/coq/pull/12018>`_,`
+  by Hugo Herbelin).`
-- 
cgit v1.2.3