Software Foundations (lf): proving leb_plus_exists and plus_leb_exists

Question

I've been working through Volume 1 of Software Foundations, and I can't get past a pair of optional questions in Logic.v. Anyone have any idea what to do?

Theorem leb_plus_exists : forall n m, n <=? m = true -> exists x, m = n+x. Proof. Admitted.

Theorem plus_exists_leb : forall n m, (exists x, m = n+x) -> n <=? m = true. Proof. (* FILL IN HERE *) Admitted.

I simple cannot get past intros in the first question. I am completely stumped on what to do.

Answer 1

Please be aware that solutions to exercises in Software Foundations, especially volume 1: Logical Foundations, are not to be published.

So, here is a hint: do induction n before you do intros m, which keeps all statements general in m.

Or, not necessary here, but if you do all intros first, then you need generalize dependent m: see generalize dependent.