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: Mar 29 2024 at 00:41 UTC