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


Last updated: Feb 08 2023 at 07:02 UTC