I ended up not needing the `leq_eq_addn`

lemma I wrote yesterday, but I still needed to prove this, and wondered if it's somewhere and I missed it:

```
From mathcomp Require Import all_ssreflect.
Open Scope order_scope.
Section Name.
Context {disp: unit} {T: orderType disp}.
Lemma seq_nonincr_iff_onestep {u: nat -> T}:
(forall n, u n.+1 <= u n) <-> (forall m n, m <= n -> u n <= u m).
Proof.
split ; last first.
move=> nonincr n.
by apply: (nonincr n n.+1).
move=> onestep m n m_le_n.
rewrite -(subnKC m_le_n).
have nameless: forall p, u (m+p) <= u m.
elim=> [ | p Hp]; first by rewrite addn0.
rewrite -addn1 addnA addn1.
apply Order.POrderTheory.le_trans with (y:= u (m+p)).
by [].
by [].
by [].
Qed.
End Name.
```

(notice that it should also come with its three brothers and sisters about increasing, decreasing and nondecreasing sequences.)

I don't think there is much about sequences in MathComp, that rather belongs to Analysis.

I have the feeling that this lemma can be seen as a variant of `telescope_big`

on booleans with `f = fun n m => u m <= u n`

and `op = (&&)`

. If this is the case, i'm not sure the proof would be shorter than a simple `elim`

though.

It is already there in the library.

```
From mathcomp Require Import all_ssreflect.
Open Scope order_scope.
Section Name.
Context {disp: unit} {T: orderType disp}.
Lemma seq_nonincr_iff_onestep {u: nat -> T}:
(forall n, u n.+1 <= u n) <-> (forall m n, m <= n -> u n <= u m).
Proof. by split=> [u_noninc m n|+ n] => [|-> //]; apply: nonincnP. Qed.
End Name.
```

One direction is trivial and the other is `nonincnP`

.

The four lemmas you were thinking about are:

```
Context {disp : unit} {T : porderType disp} [f : nat -> T].
nonincnP: (forall i : nat, f i.+1 <= f i) -> {homo f : j i / i <= j >-> j <= i}
nondecnP: (forall i : nat, f i <= f i.+1) -> {homo f : i j / i <= j >-> i <= j}
incnP: (forall i : nat, f i < f i.+1) -> {mono f : i j / i <= j >-> i <= j}
decnP: (forall i : nat, f i.+1 < f i) -> {mono f : j i / i <= j >-> j <= i}
```

And weaker variants :

```
homo_ltn_lt: (forall i : nat, f i < f i.+1) -> {homo f : i j / i < j >-> i < j}
nhomo_ltn_lt: (forall i : nat, f i.+1 < f i) -> {homo f : j i / i < j >-> j < i}
```

Ah, it was here all along! Thanks!

Julien Puydt has marked this topic as resolved.

Last updated: Jul 23 2024 at 21:01 UTC