Library prosa.util.setoid
Setoid Rewriting with boolean inequalities of ssreflect. Solution
suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016)
From Coq Require Import Basics Setoid Morphisms.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
This construction allows us to "rewrite" inequalities with ≤.
Inductive leb a b := Leb of (a ==> b).
Lemma leb_eq a b : leb a b ↔ (a → b).
Instance : PreOrder leb.
Instance : Proper (leb ==> leb ==> leb) andb.
Instance : Proper (leb ==> leb ==> leb) orb.
Instance : Proper (leb ==> impl) is_true.
Instance : Proper (le --> le ++> leb) leq.
Instance : Proper (le ==> le ==> le) addn.
Instance : Proper (le ++> le --> le) subn.
Instance : Proper (le ==> le) S.
Instance : RewriteRelation le.
Defined.
Definition leqRW {m n} : m ≤ n → le m n := leP.
To see the benefits, consider the following example.