The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

I am not sure I follow everything but it seems that in your particular
example you could use Nat.min_0_r.

More generally if you look at the documentation of under you can
handle binders :

https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html

For example, interactively this gives:

From mathcomp Require Import ssreflect.
Require Import List PeanoNat.

Goal forall l, (map (fun i => i + 1) l) = l.
Proof.
move=> l.
under map_ext => i.
  replace (i + 1) with (1 + i); last first.
    by rewrite Nat.add_comm.
  over.

Hope this helps

--
Laurent