Ssreflect Users Discussion List

[Christian Doczkal <>]

> Could you expand on what you have in mind? Do you mean that one should
> introduce a synonym for "m <= n"? Would this approach be essentially
> equivalent to 1- replacing "m <= n" with "le m n" everywhere; 2- using
> setoid rewrite on the relation le; 3- performing step 1- in reverse?

This is one way to do it. I was just toying around with your example and
here is what I ended up with:

Require Import Coq.Program.Basics. (* [flip] *)
Require Export Coq.Setoids.Setoid. (* required for [rewrite] *)
Require Export Coq.Classes.Morphisms.
Require Import Omega.

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition le n m := is_true (n <= m).

Instance le_preOrder : PreOrder le.
Proof. split. exact: leqnn. move => ? ? ?. exact: leq_trans. Qed.

Instance proper_addn: Proper (le ++> le ++> le) addn.
Proof. move => x y ? n m ?. exact: leq_add. Qed.

Instance: Coq.Classes.RelationClasses.RewriteRelation le.

Goal
  forall x y,
  x <= y ->
  x + 1 <= y + 1.
Proof.
  move => x y h. rewrite -!/(le _ _) in h *.
  rewrite h.
  reflexivity.
Qed.