Stream: math-comp users

Topic: ✔ Lemma comparing leq and addn: missing or not found?


view this post on Zulip Julien Puydt (Oct 10 2022 at 16:41):

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?

view this post on Zulip Enrico Tassi (Oct 10 2022 at 16:52):

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

view this post on Zulip Julien Puydt (Oct 10 2022 at 17:48):

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

view this post on Zulip Notification Bot (Oct 11 2022 at 13:11):

Julien Puydt has marked this topic as resolved.

view this post on Zulip Notification Bot (Oct 11 2022 at 13:11):

Julien Puydt has marked this topic as unresolved.

view this post on Zulip Notification Bot (Oct 11 2022 at 13:12):

Julien Puydt has marked this topic as resolved.


Last updated: Mar 29 2024 at 00:41 UTC