Coq, Merging two forall definitions ranging over the same types

Question

Require Import Nat.
Require Import Arith.

Theorem even_implies_div2: forall (n:nat), Nat.even n=true -> Nat.divide 2 n.
intros n H.
unfold Nat.divide.
induction n as [| n0 I0].
{ exists 0.
  reflexivity.
}
{ generalize dependent (S n0).
  generalize dependent n0.

In the above attempt, I reach to the following goal

forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2)
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

I think this should be trivially solveable. If the forall quantification is distributive over the implication, it actually becomes trivial, but my attempts to solve this failed. I tried to prove following theorems to complete the proof above.

Theorem merge_two_foralls_implies: forall (A:Type),
  forall (x0:A) (P0 P1:A-> Prop), P0 x0 -> P1 x0
  -> forall (x1:A), P0 x1 -> P1 x1.

Theorem forall_implies_distr00:
  forall (T: Type) (P0 P1: T -> Prop),
  ( forall (x:T), P0 x -> P1 x -> forall (x0: T), P0 x0
  ) <-> (
    ( forall (x:T), P0 x -> P1 x ) -> forall (x x0: T), P0 x0
  ).

Theorem dumb_prop00: forall (P0 P1: Prop),
  (P0 -> P1 -> P0) -> (P0 -> P1) <-> P0. (* This seems wrong *)

Answer 1

You seem to be confusing

forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2)
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

with

(forall n0 : nat,
(Nat.even n0 = true -> exists z : nat, n0 = z * 2))
->
forall n : nat,
Nat.even n = true -> exists z : nat, n = z * 2

The second proof is indeed trivial:

Goal (forall n0 : nat,
     (Nat.even n0 = true -> exists z : nat, n0 = z * 2)) ->
forall n : nat, Nat.even n = true -> exists z : nat, n = z * 2.
Proof.
  trivial.
Qed.

whereas the first proof is not. Note carefully the extra pair of parentheses in the second.

Here is an explicit example where you provably cannot distribute the forall quantification over implication:

Goal ~ forall n : nat, n <> 1 -> (forall n : nat, n <> 1).
Proof.
  intros H.
  now contradiction (H _ (n_Sn 0) 1).
Qed.

Contrast with

Goal (forall n : nat, n <> 1) -> (forall n : nat, n <> 1).
Proof.
  intro.
  assumption.
Qed.