I've been unable to find the following lemma:

```
Lemma leq_eq_addn: forall m n, m <= n <-> exists p, n = m + p.
Proof.
split ; last first.
move=> [p Hp].
rewrite Hp.
apply: leq_addr.
move=> H.
exists (n - m).
rewrite subnKC //=.
Qed.
```

I have to admit my searching skills aren't very good... was it somewhere and I missed it?

look for n = m + (n - m) or similar

Well, I did find subnKC -- which I used to prove the lemma, but that's not what I was looking for

Julien Puydt has marked this topic as resolved.

Julien Puydt has marked this topic as unresolved.

Julien Puydt has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC