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 distributes 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 *)

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 *)