Proving weaker exists based on forall

Question

Lemma one_bigger' : forall n h, 
   n = S (double h) -> (exists k, S n = double k).
Proof.
  intros n h H.  rewrite H. exists (S h). reflexivity.
Qed.

Lemma one_bigger : forall n, 
   (exists k, n = S (double k)) -> (exists k, S n = double k).
Admitted.

It seems to me that the second lemma should be trivially provable given the first, but I can't seem to wrap my head around how to use the first lemma to prove the second one.

Answer 1

case H seems to be the magic I couldn't find:

Lemma one_bigger : forall n, 
   (exists k, n = S (double k)) -> (exists k, S n = double k).
Proof.
  intros n H. case H. apply one_bigger'.
Qed.

Answer 2

Indeed, your example is an instance of an equivalence (Lemma L)

Section S1.
  Variable (A :Type).
  Variables (P : A -> Prop) (Q:  Prop).
  
  Lemma L : (forall x , P x  -> Q ) <-> ((exists x, P x) -> Q). 
   Proof.
    split.
    - intros H [x Hx]; now apply (H x).
    - intros H x Hx; apply H. now exists x.
  Qed.
End S1.

Lemma one_bigger'' : forall n, 
    (exists k, n = S (double k)) -> (exists k, S n = double k).
Proof. 
  intros n .
  rewrite <- L . 
  apply one_bigger'. 
Qed. 

Answer 3

If you use SSReflect, you can write your proof as follows.

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma one_bigger' : forall n h, 
   n = S (double h) -> (exists k, S n = double k).
Proof.
  intros n h H.  rewrite H. exists (S h). reflexivity.
Qed.

Lemma one_bigger : forall n, 
   (exists k, n = S (double k)) -> (exists k, S n = double k).
Proof. by move=> n [k /one_bigger']. Qed.

The move construct does the same as intros, except that your H is here directly destructured into a witness, k, and a proof of the equality in the existential. This last proof is directly passed to one_bigger' via the / notation, thus yielding the expected result.

Another, more explicit proof would be

Proof. move=> n [k eqn]. exists k.+1. by rewrite eqn doubleS. Qed.