Partial proof that Axiom of Choice --> Law of Excluded Middle in Coq

AOC_LEM.v

Require Import Coq.Logic.ClassicalChoice.

Definition two (n : nat) : Prop := n = 0 \/ n = 1.

Lemma zero_in_two : two 0.
Proof.
  unfold two. left. reflexivity.
Qed.

Lemma one_in_two : two 1.
Proof.
  unfold two. right. reflexivity.
Qed.

Definition A (n : nat) (P : Prop) (x : two n) : Prop := n = 0 \/ P.

Lemma zero_in_A : forall (P : Prop), A 0 P zero_in_two.
Proof.
  intros.
  unfold A.
  left. reflexivity.
Qed.

Definition B (n : nat) (P : Prop) (x : two n) : Prop := n = 1 \/ P.

Lemma one_in_B : forall (P : Prop), B 1 P one_in_two.
Proof.
  intros.
  unfold B.
  left. reflexivity.
Qed.

(* What should this be? *)
Definition R (n : nat) (n' : nat) (P : Prop) (x : two n) (y : two n') (a : A n P x) (b : B n' P y) : Prop := (n = 0 /\ n' = 1) \/ P.

(* How to prove this? Is this actually the inhabitation statement? *)
Lemma inhabited : forall (n : nat) (n' : nat) (P : Prop) (x : two n) (y : two n'), 
    (forall a : A n P x, exists b : B n' P y, R n n' P x y a b).
Admitted.

Theorem choiceABR : forall (n : nat) (n' : nat) (P : Prop) (x : two n) (y : two n'),
    exists f : A n P x -> B n' P y, (forall a : A n P x, R n n' P x y a (f a)).
  intros.
  apply choice.
  apply inhabited.
Qed.

Theorem lem : forall (P : Prop), P \/ ~P.
Admitted.