(* Author: Christian Doczkal *)
(* Distributed under the terms of CeCILL-B. *)
From Coq Require Import Basics Setoid Morphisms.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* Distributed under the terms of CeCILL-B. *)
From Coq Require Import Basics Setoid Morphisms.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Setoid Rewriting with Ssreflec's boolean inequalities.
Solution suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016)Inductive leb a b := Leb of (a ==> b).
Lemma leb_eq a b : leb a b <-> (a -> b).
Proof. move: a b => [|] [|]; firstorder. Qed.
Instance: PreOrder leb.
Proof. split => [[|]|[|][|][|][?][?]]; try exact: Leb. Qed.
Instance: Proper (leb ==> leb ==> leb) andb.
Proof. move => [|] [|] [A] c d [B]; exact: Leb. Qed.
Instance: Proper (leb ==> leb ==> leb) orb.
Proof. move => [|] [|] [A] [|] d [B]; exact: Leb. Qed.
Instance: Proper (leb ==> impl) is_true.
Proof. move => a b []. exact: implyP. Qed.
Instances for le
Instance: Proper (le --> le ++> leb) leq.
Proof. move => n m /leP ? n' m' /leP ?. apply/leb_eq => ?. eauto using leq_trans. Qed.
Instance: Proper (le ==> le ==> le) addn.
Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_add. Qed.
Instance: Proper (le ==> le ==> le) muln.
Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_mul. Qed.
Instance: Proper (le ++> le --> le) subn.
Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_sub. Qed.
Instance: Proper (le ==> le) S.
Proof. move => n m /leP ?. apply/leP. by rewrite ltnS. Qed.
Instance: RewriteRelation le := Build_RewriteRelation _.
Wrapper Lemma to trigger setoid rewrite
Testing