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.
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.