#### The one place for your designs

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.

The setoid rewriting mechanism uses a bunch of typeclass machinery to infer `Proper`

instances for the contexts being rewritten in, and it uses `flip`

to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes `flip`

typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In `base.v`

, we have:

`Typeclasses Transparent id compose flip const.`

This nullifies the effect of the very first non-comment non-import line of `Classes/Init.v`

in the Coq stdlib:

`Typeclasses Opaque id const flip compose arrow impl iff not all.`

Here's a minimal demonstration of the problems this causes:

```
From Coq Require Import ssreflect ssrfun ssrbool.
Require Import Morphisms.
Require Import PeanoNat.
Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
Require Import stdpp.base.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
Fail setoid_rewrite <- H1 in H2 at 1.
Abort.
Section FlippedInstance.
(* Thus seemingly necessitating: *)
Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
End FlippedInstance.
(* But alternatively: *)
Typeclasses Opaque flip.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
```

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.