Adding properties about implb.

This addresses a question on gitter (April 4).

1 files changed, 19 insertions, 0 deletions

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).`