Section Useful_Lemma.

Theorem Add_related_quanteur :
 forall (T : Type) (P : T -> Prop) (t : T), (forall t : T, P t) -> P t.
Proof.
intros. apply H.
Qed.

Theorem Merge_quanteurs :
 forall (T : Type) (P Q : T -> Prop),
 (forall t : T, P t -> Q t) -> (forall t : T, P t) -> forall t : T, Q t.
intros.
auto.
Qed.

Theorem Merge_quanteurs3 :
 forall (T : Type) (P Q : T -> T -> T -> Prop),
 (forall x y z : T, P x y z -> Q x y z) ->
 (forall x y z : T, P x y z) -> forall x y z : T, Q x y z.
intros.
auto.
Qed.

Theorem SplitInTail :
 forall P Q R : Prop, (P -> Q) -> (P -> R) -> P -> Q /\ R.
Proof.
intros.
split; [ apply H | apply H0 ]; assumption.
Qed.

Theorem SplitInHead : forall P Q R : Prop, (P -> Q -> R) -> P /\ Q -> R.
Proof.
intros.
decompose [and] H0.
auto.
Qed.

Theorem PIP : forall P : Prop, P -> P.
Proof.
intros P p; apply p.
Qed.

Theorem MP : forall P Q : Prop, (P -> Q) -> P -> Q.
Proof.
intros; apply H; exact H0.
Qed.

Theorem DeepSplit1 :
 forall P1 P2 Q1 Q2 R1 R2 S11 S12 : Prop,
 (S11 -> S12 -> R1) ->
 (P1 -> Q1 -> S11) /\ (P2 -> Q2 -> R2) ->
 (P1 -> Q1 -> S12) /\ (P2 -> Q2 -> R2) ->
 (P1 -> Q1 -> R1) /\ (P2 -> Q2 -> R2).
Proof.
intros until S12.
intros.
decompose [and] H0; decompose [and] H1; clear H0 H1.
split.
2: assumption.
intros; apply H.
apply H2; assumption.
apply H4; assumption.
Qed.

Theorem DeepSplit2 :
 forall P1 P2 Q1 Q2 R1 R2 S21 S22 : Prop,
 (S21 -> S22 -> R2) ->
 (P1 -> Q1 -> R1) /\ (P2 -> Q2 -> S21) ->
 (P1 -> Q1 -> R1) /\ (P2 -> Q2 -> S22) ->
 (P1 -> Q1 -> R1) /\ (P2 -> Q2 -> R2).
Proof.
intros until S22.
intros.
decompose [and] H0; decompose [and] H1; clear H0 H1.
split.
assumption.
intros; apply H.
apply H3; assumption.
apply H5; assumption.
Qed.

Theorem raise_quantifier : forall (T:Type) (P:Prop) (Q:T->Prop), (forall (t:T), P -> (Q t)) -> P -> forall (t:T), Q t.
Proof.
intros T P Q H p t.
apply H.
exact p.
Qed.

Theorem SplitInBoth:
  forall P Q R S : Prop,
    (P -> R) /\ (Q -> S) ->
    (P /\ Q) -> (R /\ S).
Proof.
intros P Q R S [PR QS] [p q].
split; auto.
Qed.

End Useful_Lemma.

Inductive Game : Type :=
    Game_cons : forall LI RI : Type, (LI -> Game) -> (RI -> Game) -> Game.

(* The projections *)
Definition GLeftIndex (G : Game) :=
  match G with
  | Game_cons A B f g => A
  end.
Definition GRightIndex (G : Game) :=
  match G with
  | Game_cons A B f g => B
  end.
Definition GLeftFun (G : Game) :=
  match G return (GLeftIndex G -> Game) with
  | Game_cons A B f g => f
  end.
Definition GRightFun (G : Game) :=
  match G return (GRightIndex G -> Game) with
  | Game_cons A B f g => g
  end.

(* Induction schemes to be used later *)
Theorem Rol3Induction :
 forall P : Game -> Game -> Game -> Prop,
 (forall x y z : Game,
  (forall xli : GLeftIndex x, let xl := GLeftFun x xli in P y z xl) ->
  (forall zri : GRightIndex z, let zr := GRightFun z zri in P zr x y) ->
  P x y z) -> forall x y z : Game, P x y z.
intros P IH.
exact
 (fix pc0 (x y z : Game) {struct z} :
    P x y z :=
  (* auxpc{0,1} x y == (pc{0,1} x y z) *)
  let auxpc1 := (fix auxpc1 (x y : Game) {struct x} : P y z x :=
         let auxpc0 :=
           fun x y : Game =>
           IH x y z
             (fun xli : GLeftIndex x =>
              let xl := GLeftFun x xli in auxpc1 xl y)
             (fun zri : GRightIndex z =>
              let zr := GRightFun z zri in (*<(P zr x y)>*)
              IH zr x y
                (fun zrli : GLeftIndex zr =>
                 let zrl := GLeftFun zr zrli in pc0 x y zrl)
                (fun yri : GRightIndex y =>
                 let yr := GRightFun y yri in pc1 x yr zr))
           (* auxauxpc1 == auxpc1 x*)
            in
         let auxauxpc1 := (fix auxauxpc1 (y : Game) : P y z x :=
                IH y z x
                  (fun yli : GLeftIndex y =>
                   let yl := GLeftFun y yli in (*<(P z x yl)>*)
                   IH z x yl
                     (fun zli : GLeftIndex z =>
                      let zl := GLeftFun z zli in pc0 x yl zl)
                     (fun ylri : GRightIndex yl =>
                      let ylr := GRightFun yl ylri in auxauxpc1 ylr))
                  (fun xri : GRightIndex x =>
                   let xr := GRightFun x xri in auxpc0 xr y)) in
         IH y z x
           (fun yli : GLeftIndex y =>
            let yl := GLeftFun y yli in (*<(P z x yl)>*)
            IH z x yl
              (fun zli : GLeftIndex z =>
               let zl := GLeftFun z zli in pc0 x yl zl)
              (fun ylri : GRightIndex yl =>
               let ylr := GRightFun yl ylri in auxauxpc1 ylr))
           (fun xri : GRightIndex x =>
            let xr := GRightFun x xri in auxpc0 xr y)) in
  IH x y z
    (fun xli : GLeftIndex x => let xl := GLeftFun x xli in auxpc1 xl y)
    (fun zri : GRightIndex z =>
     let zr := GRightFun z zri in (*<(P zr x y)>*)
     IH zr x y
       (fun zrli : GLeftIndex zr =>
        let zrl := GLeftFun zr zrli in pc0 x y zrl)
       (fun yri : GRightIndex y => let yr := GRightFun y yri in pc1 x yr zr))
  with pc1 (x y z : Game) {struct z} :
    P y z x :=
  (* auxpc{0,1} x y == (pc{0,1} x y z) *)
  let auxpc1 := (fix auxpc1 (x y : Game) {struct x} : P y z x :=
         let auxpc0 :=
           fun x y : Game =>
           IH x y z
             (fun xli : GLeftIndex x =>
              let xl := GLeftFun x xli in auxpc1 xl y)
             (fun zri : GRightIndex z =>
              let zr := GRightFun z zri in (*<(P zr x y)>*)
              IH zr x y
                (fun zrli : GLeftIndex zr =>
                 let zrl := GLeftFun zr zrli in pc0 x y zrl)
                (fun yri : GRightIndex y =>
                 let yr := GRightFun y yri in pc1 x yr zr)) in
         let auxauxpc1 := (fix auxauxpc1 (y : Game) : P y z x :=
                IH y z x
                  (fun yli : GLeftIndex y =>
                   let yl := GLeftFun y yli in (*<(P z x yl)>*)
                   IH z x yl
                     (fun zli : GLeftIndex z =>
                      let zl := GLeftFun z zli in pc0 x yl zl)
                     (fun ylri : GRightIndex yl =>
                      let ylr := GRightFun yl ylri in auxauxpc1 ylr))
                  (fun xri : GRightIndex x =>
                   let xr := GRightFun x xri in auxpc0 xr y)) in
         IH y z x
           (fun yli : GLeftIndex y =>
            let yl := GLeftFun y yli in (*<(P z x yl)>*)
            IH z x yl
              (fun zli : GLeftIndex z =>
               let zl := GLeftFun z zli in pc0 x yl zl)
              (fun ylri : GRightIndex yl =>
               let ylr := GRightFun yl ylri in auxauxpc1 ylr))
           (fun xri : GRightIndex x =>
            let xr := GRightFun x xri in auxpc0 xr y)) in
  let auxpc0 :=
    fun x y : Game =>
    IH x y z
      (fun xli : GLeftIndex x => let xl := GLeftFun x xli in auxpc1 xl y)
      (fun zri : GRightIndex z =>
       let zr := GRightFun z zri in (*<(P zr x y)>*)
       IH zr x y
         (fun zrli : GLeftIndex zr =>
          let zrl := GLeftFun zr zrli in pc0 x y zrl)
         (fun yri : GRightIndex y => let yr := GRightFun y yri in pc1 x yr zr)) in
  IH y z x
    (fun yli : GLeftIndex y =>
     let yl := GLeftFun y yli in (*<(P z x yl)>*)
     IH z x yl
       (fun zli : GLeftIndex z => let zl := GLeftFun z zli in pc0 x yl zl)
       (fun ylri : GRightIndex yl =>
        let ylr := GRightFun yl ylri in auxpc1 x ylr))
    (fun xri : GRightIndex x => let xr := GRightFun x xri in auxpc0 xr y)
  for pc0).
Qed.


Theorem Roll3Induction :
 forall P P1 P2 : Game -> Game -> Prop,
 let F := fun x y z : Game => P x y -> P y z -> P x z in
 (forall x z : Game,
  (forall xli : GLeftIndex x, let xl := GLeftFun x xli in P1 xl z) ->
  (forall zri : GRightIndex z, let zr := GRightFun z zri in P2 x zr) -> P x z) ->
 (forall x z : Game,
  P x z ->
  (forall xli : GLeftIndex x, let xl := GLeftFun x xli in P1 xl z) /\
  (forall zri : GRightIndex z, let zr := GRightFun z zri in P2 x zr)) ->
 (forall x y z : Game, P1 x y -> P y z -> F y z x -> P1 x z) ->
 (forall x y z : Game, P2 y z -> P x y -> F z x y -> P2 x z) ->
 forall x y z : Game, F x y z.
intros P P1 P2 F P12P PP12 p1 p2.
intros x y z.
eapply Rol3Induction with (P := F).
clear x y z.
intros x y z.
intros IH1 IH2.
intros xy yz.
apply P12P.

intros xli xl.
eapply p1.
2: apply yz.
2: apply IH1 with (xli := xli).
(* P1 xl y derives from (P x y) *)

elim (PP12 _ _ xy); intros P1xly _.
apply (P1xly xli).

intros zri zr.
eapply p2.
2: apply xy.
2: apply IH2 with (zri := zri).

elim (PP12 _ _ yz); intros _ P1yzr.
apply (P1yzr zri).
Qed.

Definition EmptyGameSet : False -> Game.
Proof.
intro.
contradiction.
Defined.

Inductive OnePointIndex : Set :=
    OnePoint : OnePointIndex.

Inductive sumT (A B : Type) : Type :=
  | inlT : A -> sumT A B
  | inrT : B -> sumT A B.

Definition map_on_sumT (A B C : Type) (fa : A -> C) 
  (fb : B -> C) (x : sumT A B) :=
  match x with
  | inlT e => fa e
  | inrT e => fb e
  end.

Inductive GMult_prodT (A : Type) (B : Type) : Type :=
  GMult_pairT : A -> B -> GMult_prodT A B.

Implicit Arguments GMult_pairT [A B].

(* The following two are a kind of "for all":
   They calculate wether
   PR (resp. PL) is true on their third argument
   PL (resp. PR) is true on the left (resp. right) elements of it
   etc, alternating
 *)

Fixpoint RecurseAlternateLeft (PL PR : Game -> Prop) 
 (g2 : Game) {struct g2} : Prop :=
  let (LI, RI, Lf, Rf) return Prop := g2 in
  (forall l : LI, RecurseAlternateRight PL PR (Lf l)) /\ PR g2
 
 with RecurseAlternateRight (PL PR : Game -> Prop) 
 (g2 : Game) {struct g2} : Prop :=
  let (LI, RI, Lf, Rf) return Prop := g2 in
  (forall r : RI, RecurseAlternateLeft PL PR (Rf r)) /\ PL g2.

Theorem RecurseAlternateLeftThusLevel1 :
 forall (PL PR : Game -> Prop) (g : Game),
 RecurseAlternateLeft PL PR g -> PR g.
Proof.
intros PL PR g.
case g.
intros LI RI Lf Rf.
simpl in |- * .
apply proj2.
Qed.

Definition Zero := Game_cons False False EmptyGameSet EmptyGameSet.
Definition One :=
  Game_cons OnePointIndex False (fun x : OnePointIndex => Zero) EmptyGameSet.

Inductive Glte : Game -> Game -> Prop :=
    Glte_cons :
      forall x y:Game,
      (forall xli : (GLeftIndex  x), NGgte (GLeftFun x xli)  y) ->
      (forall yri : (GRightIndex y), NGgte x (GRightFun y yri)) -> Glte x y
with NGgte : Game -> Game -> Prop :=
  | NGgte_xr :
      forall x y : Game,
      ex (fun xri : (GRightIndex x) => Glte (GRightFun x xri)  y) -> NGgte x y
  | NGgte_yl :
      forall x y : Game,
      ex (fun yli : (GLeftIndex y)  => Glte x (GLeftFun y yli)) -> NGgte x y.

Fixpoint AntiGame (g : Game) : Game :=
  match g with
  | Game_cons LI RI Lf Rf =>
      Game_cons RI LI (fun i : RI => AntiGame (Rf i))
        (fun i : LI => AntiGame (Lf i))
  end.

Fixpoint GPlus (x y : Game) {struct x} : Game :=
  let GPlusAux :=
    (fix GPlusAux (z : Game) : Game :=
      Game_cons (sumT (GLeftIndex x) (GLeftIndex z)) (sumT (GRightIndex x) (GRightIndex z))
      (map_on_sumT (GLeftIndex x) (GLeftIndex z) Game
        (fun xli : (GLeftIndex x) => GPlus (GLeftFun x xli) z)
        (fun zli : (GLeftIndex z) => GPlusAux (GLeftFun z zli)))
      (map_on_sumT (GRightIndex x) (GRightIndex z) Game
        (fun xri : (GRightIndex x) => GPlus (GRightFun x xri) z)
        (fun zri : (GRightIndex z) => GPlusAux (GRightFun z zri))))
    in
    (GPlusAux y).

Definition GPlusAux (x : Game) :=
  (fix GPlusAux (z : Game) : Game :=
    Game_cons (sumT (GLeftIndex x) (GLeftIndex z)) (sumT (GRightIndex x) (GRightIndex z))
    (map_on_sumT (GLeftIndex x) (GLeftIndex z) Game
      (fun xli : (GLeftIndex x) => GPlus (GLeftFun x xli) z)
      (fun zli : (GLeftIndex z) => GPlusAux (GLeftFun z zli)))
    (map_on_sumT (GRightIndex x) (GRightIndex z) Game
      (fun xri : (GRightIndex x) => GPlus (GRightFun x xri) z)
      (fun zri : (GRightIndex z) => GPlusAux (GRightFun z zri)))).

Theorem GPlusxGPlusAux :
 forall x y : Game,
    (GPlus x y) = (GPlusAux x y).
Proof.
intros x y.
case x.
intros xLI xRI xLf xRf.
case y.
intros yLI yRI yLf yRf.
clear x y.
reflexivity.
Qed.

Theorem IS :
 forall P : Game -> Game -> Prop,
 (forall x y : Game,
  (forall yli : GLeftIndex y, let yl := GLeftFun y yli in P x yl) ->
  (forall xri : GRightIndex x, let xr := GRightFun x xri in P xr y) -> P x y) ->
 forall x y : Game, P x y.
intros P IH.
exact
 (fix pc (x y : Game) {struct x} : P x y :=
    let auxpc := (fix auxpc (z : Game) : P x z :=
           IH x z
             (fun zli : GLeftIndex z => let zl := GLeftFun z zli in auxpc zl)
             (fun xri : GRightIndex x => let xr := GRightFun x xri in pc xr z)) in
    IH x y (fun yli : GLeftIndex y => let yl := GLeftFun y yli in auxpc yl)
      (fun xri : GRightIndex x => let xr := GRightFun x xri in pc xr y)).
Qed.

Theorem IS2 :
 forall P : Game -> Game -> Prop,
 (forall x y : Game,
  (forall yli : GLeftIndex y, let yl := GLeftFun y yli in P yl x) ->
  (forall xri : GRightIndex x, let xr := GRightFun x xri in P y xr) -> P x y) ->
 forall x y : Game, P x y.
intros P IH.
exact
 (fix pc (x y : Game) {struct x} : P x y :=
    let xLI := GLeftIndex x in
    let yRI := GRightIndex y in
    let xRI := GRightIndex x in
    let yLI := GLeftIndex y in
    let auxpc := (fix auxpc (z : Game) : P x z :=
           let zRI := GRightIndex z in
           let zLI := GLeftIndex z in
           IH x z
             (fun zli : zLI =>
              let zl := GLeftFun z zli in
              IH zl x (fun xli : xLI => let xl := GLeftFun x xli in pc xl zl)
                (fun zlri : GRightIndex zl =>
                 let zlr := GRightFun zl zlri in auxpc zlr))
             (fun xri : xRI =>
              let xr := GRightFun x xri in
              IH z xr
                (fun xrli : GLeftIndex xr =>
                 let xrl := GLeftFun xr xrli in pc xrl z)
                (fun zri : zRI => let zr := GRightFun z zri in pc xr zr))) in
    IH x y
      (fun yli : yLI =>
       let yl := GLeftFun y yli in
       IH yl x (fun xli : xLI => let xl := GLeftFun x xli in pc xl yl)
         (fun ylri : GRightIndex yl =>
          let ylr := GRightFun yl ylri in auxpc ylr))
      (fun xri : xRI =>
       let xr := GRightFun x xri in
       IH y xr
         (fun xrli : GLeftIndex xr => let xrl := GLeftFun xr xrli in pc xrl y)
         (fun yri : yRI => let yr := GRightFun y yri in pc xr yr))).
Qed.

(* This one is IS2, swapping x and y in the premises, but not in the conclusion *)

Theorem IS2Reverse :
 forall P : Game -> Game -> Prop,
 (forall x y : Game,
  (forall xli : GLeftIndex x, let xl := GLeftFun x xli in P y xl) ->
  (forall yri : GRightIndex y, let yr := GRightFun y yri in P yr x) -> P x y) ->
 forall x y : Game, P x y.
Proof.
intros P IH.
exact
 (fix pc (x y : Game) {struct x} : P x y :=
    let xLI := GLeftIndex x in
    let yRI := GRightIndex y in
    let xRI := GRightIndex x in
    let yLI := GLeftIndex y in
    let auxpc := (fix auxpc (z : Game) : P x z :=
           let zRI := GRightIndex z in
           let zLI := GLeftIndex z in
           IH x z
             (fun xli : xLI =>
              let xl := GLeftFun x xli in
              IH z xl (fun zli : zLI => let zl := GLeftFun z zli in pc xl zl)
                (fun xlri : GRightIndex xl =>
                 let xlr := GRightFun xl xlri in pc xlr z))
             (fun zri : zRI =>
              let zr := GRightFun z zri in
              IH zr x
                (fun zrli : GLeftIndex zr =>
                 let zrl := GLeftFun zr zrli in auxpc zrl)
                (fun xri : xRI => let xr := GRightFun x xri in pc xr zr))) in
    IH x y
      (fun xli : xLI =>
       let xl := GLeftFun x xli in
       IH y xl (fun yli : yLI => let yl := GLeftFun y yli in pc xl yl)
         (fun xlri : GRightIndex xl =>
          let xlr := GRightFun xl xlri in pc xlr y))
      (fun yri : yRI =>
       let yr := GRightFun y yri in
       IH yr x
         (fun yrli : GLeftIndex yr =>
          let yrl := GLeftFun yr yrli in auxpc yrl)
         (fun xri : xRI => let xr := GRightFun x xri in pc xr yr))).
Qed.

Theorem NGgteIsNGgte_Step :
  forall x y : Game,
    (forall yli : (GLeftIndex  y), let yl := GLeftFun  y yli in NGgte yl x -> ~ Glte x yl) ->
    (forall xri : (GRightIndex x), let xr := GRightFun x xri in NGgte y xr -> ~ Glte xr y) ->
 NGgte x y -> ~ Glte y x.
Proof.
intros x y IHyl IHxr.
intros NGxy Lyx.
inversion NGxy as [x' y' smallxr_ex x'x y'y | x' y' bigyl_ex x'x y'y ]; clear x' y' x'x y'y NGxy;
  [clear IHyl | clear IHxr]; inversion Lyx as [y' x' All_NGylx All_NGyxr y'y x'x]; clear x' y' x'x y'y.

elim smallxr_ex; clear smallxr_ex.
intros smallxr smallxr_is_small.
apply IHxr with (xri := smallxr).
apply All_NGyxr.
exact smallxr_is_small.

elim bigyl_ex; clear bigyl_ex.
intros bigyl bigyl_is_big.
apply IHyl with (yli := bigyl).
apply All_NGylx.
exact bigyl_is_big.
Qed.

Theorem NGgteIsNGgte : forall x y : Game, NGgte x y -> ~ Glte y x.
intros x y.
eapply IS2 with (P := fun a b : Game => NGgte a b -> ~ Glte b a).
clear x y.
intros x y.
apply NGgteIsNGgte_Step; assumption.
Qed.

Theorem NGgteGgteAbsurd : forall x y : Game, NGgte x y -> Glte y x -> False.
exact NGgteIsNGgte.
Qed.

Theorem NGgteToProp :
 forall x y : Game,
 NGgte x y ->
 ex (fun r : GRightIndex x => Glte (GRightFun x r) y) \/
 ex (fun l : GLeftIndex y => Glte x (GLeftFun y l)).
Proof.
intros x y xy.
elim xy; clear x y xy; intros x y; auto.
Qed.

Theorem NNGgteToProp :
 forall x y : Game,
 ~ NGgte x y ->
 (forall r : GRightIndex x, ~ Glte (GRightFun x r) y) /\
 (forall l : GLeftIndex y, ~ Glte x (GLeftFun y l)).
Proof.
intros x y nnxy.
split.

intros xri xry.
apply nnxy.
constructor 1.
exists xri.
exact xry.

intros yli xyl.
apply nnxy.
constructor 2.
exists yli.
exact xyl.
Qed.

Axiom Classic : forall P : Prop, ~ ~ P -> P.

Theorem NGgteNGgte : forall x y : Game, ~ NGgte x y -> Glte y x.
intros x y.
eapply IS2 with (P := fun a b : Game => ~ NGgte a b -> Glte b a).
clear x y.
intros x y.
intros IHy IHx NNyx.

assert (NNyx_1:forall xri : GRightIndex x, ~ Glte (GRightFun x xri) y).
elim (NNGgteToProp x y NNyx); auto.
assert (NNyx_2:forall yli : GLeftIndex y, ~ Glte x (GLeftFun  y yli)).
elim (NNGgteToProp x y NNyx); auto.

exists.
intros yli.
apply Classic.
intro nnylx.
apply NNyx_2 with (yli := yli).
apply IHy.
exact nnylx.

intros xri.
apply Classic.
intro nnyxr.
apply (NNyx_1 xri).
apply IHx.
exact nnyxr.
Qed.

Theorem nGlteNGgte : forall x y : Game, ~ Glte x y -> NGgte y x.
Proof.
intros x y nxy.
apply Classic; intros nNyx.
apply nxy.
apply NGgteNGgte.
assumption.
Qed.

Theorem GltexryGlteyxAbsurd :
 forall x y : Game,
 forall xri : GRightIndex x, Glte (GRightFun x xri) y -> Glte y x -> False.
intros x y xri xry yx.
inversion yx as [y' x' Nylx Nyxr y'y x'x].
clear y' x' y'y x'x.
eapply NGgteGgteAbsurd.
2: apply yx.
apply NGgte_xr.
exists xri.
exact xry.
Qed.

Theorem Glte_transitive :
 forall x z y : Game, Glte x y -> Glte y z -> Glte x z.
Proof.
intros x y z.
apply
 Roll3Induction
                with
                (P := fun x y : Game => Glte x y)
               (P1 := fun x y : Game => NGgte x y)
               (P2 := fun x y : Game => NGgte x y);
clear x y z.
intros x z.
intros Hxl Hzr.
exists.
exact Hxl.
exact Hzr.

intros x z.
intros xz.
inversion xz as [x' z' Nxlz Nxzr x'x z'z]; clear x' z' x'x z'z.
split; assumption.

intros x y z.
intros xy yz Trans.
apply nGlteNGgte.
intro zx.
absurd (Glte y x).
apply NGgteIsNGgte.
assumption.
apply Trans; assumption.

intros x y z.
intros yz xy Trans.
apply nGlteNGgte.
intro zx.
absurd (Glte z y).
apply NGgteIsNGgte.
assumption.
apply Trans; assumption.
Qed.

Theorem Glte_reflexive : forall x : Game, Glte x x.
intros.
induction x as [LI RI Lf LIH Rf RIH].
set (x := Game_cons LI RI Lf Rf) in |- * .
exists.

intros xli.
constructor 2.
exists xli.
apply LIH.

intros xri.
constructor 1.
exists xri.
apply RIH.
Qed.

(* Glte is a pre-order *)

Definition Geq (x y : Game) : Prop := Glte x y /\ Glte y x.

Theorem Geq_symmetric : forall x y : Game, Geq x y -> Geq y x.
Proof.
intros x y [xy yx].
split; [exact yx | exact xy] .
Qed.

Theorem Geq_transitive : forall x y z : Game, Geq x y -> Geq y z -> Geq x z.
Proof.
intros x y z [xy yx] [yz zy].
split; apply Glte_transitive with (y := y); assumption.
Qed.

Theorem Geq_reflexive : forall x : Game, Geq x x.
Proof.
intros x.
split; apply Glte_reflexive.
Qed.

Inductive Gidentical : Game -> Game -> Prop :=
    Gidentical_cons :
      forall x y : Game,
      (forall xli : GLeftIndex x,
       ex
         (fun yli : GLeftIndex y =>
          Gidentical (GLeftFun x xli) (GLeftFun y yli))) ->
      (forall xri : GRightIndex x,
       ex
         (fun yri : GRightIndex y =>
          Gidentical (GRightFun x xri) (GRightFun y yri))) ->
      (forall yli : GLeftIndex y,
       ex
         (fun xli : GLeftIndex x =>
          Gidentical (GLeftFun y yli) (GLeftFun x xli))) ->
      (forall yri : GRightIndex y,
       ex
         (fun xri : GRightIndex x =>
          Gidentical (GRightFun y yri) (GRightFun x xri))) -> 
      Gidentical x y.

Theorem Gidentical_reflexive : forall x : Game, Gidentical x x.
Proof.
intro x.
induction x as [LI RI Lf LIH Rf RIH].
set (x := Game_cons LI RI Lf Rf) in |- * .
cut
 (forall xli : GLeftIndex x,
  exists yli : GLeftIndex x, Gidentical (GLeftFun x xli) (GLeftFun x yli)).
intro HL.
cut
 (forall xri : GRightIndex x,
  exists yri : GRightIndex x, Gidentical (GRightFun x xri) (GRightFun x yri)).
intro HR.
exists;
 [ exact HL | exact HR | exact HL | exact HR ].
clear HL.
intro xri.
exists xri.
apply RIH.
intro xli; exists xli; apply LIH.
Qed.

Theorem Gidentical_commutative :
 forall x y : Game, Gidentical y x -> Gidentical x y.
intros x y yx.
elim yx. clear x y yx.
intros x y ylH yrH xlH xrH.
exists; assumption.
Qed.

Theorem Gidentical_transitive :
 forall x y z : Game, Gidentical x y -> Gidentical y z -> Gidentical x z.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y z xy yz.
inversion xy as [x' y' xylH xyrH yxlH yxrH xx' yy'].
clear x' y' xx' yy'.
inversion yz as [y' z' yzlH yzrH zylH zyrH yy' zz'].
clear y' z' yy' zz'.
exists.

intros xli.
elim (xylH xli).
intros yli xylHi.
elim (yzlH yli).
intros zli yzlHi.
exists zli.
eapply xLIH; [ apply xylHi | apply yzlHi ].

intros xri.
elim (xyrH xri).
intros yri xyrHi.
elim (yzrH yri).
intros zri yzrHi.
exists zri.
eapply xRIH; [ apply xyrHi | apply yzrHi ].

intros zli.
elim (zylH zli).
intros yli zylHi.
elim (yxlH yli).
intros xli yxlHi.
exists xli.
apply Gidentical_commutative.
eapply xLIH; apply Gidentical_commutative; [ apply yxlHi | apply zylHi ].

intros zri.
elim (zyrH zri).
intros yri zyrHi.
elim (yxrH yri).
intros xri yxrHi.
exists xri.
apply Gidentical_commutative.
eapply xRIH; apply Gidentical_commutative; [ apply yxrHi | apply zyrHi ].
Qed.

Theorem GidGeq: forall x y:Game, (Gidentical x y) -> (Geq x y).
Proof.
intro x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y idxy.
inversion idxy as [x' y' xlyl xryr ylxl yrxr x'x y'y]; clear x' y' x'x y'y idxy.
split; exists.

constructor 2.
elim (xlyl xli).
intro yli.
intro idxlyl.
exists yli.
eapply proj1; apply xLIH.
exact idxlyl.

constructor 1.
elim (yrxr yri).
intro xri.
intro idyrxr.
exists xri.
eapply proj1; apply xRIH.
apply Gidentical_commutative.
exact idyrxr.

intro yli.
constructor 2.
elim (ylxl yli).
intro xli.
intro idylxl.
exists xli.
eapply proj2; apply xLIH.
apply Gidentical_commutative.
exact idylxl.

intro xri.
constructor 1.
elim (xryr xri).
intro yri.
intro idxryr.
exists yri.
eapply proj2; apply xRIH.
exact idxryr.
Qed.

Theorem GidGlte: forall x y:Game, (Gidentical x y) -> (Glte x y).
Proof.
intro x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y xy.
exists.

intros xli.
right.
inversion xy as [x' y' xlyl xryr ylxl yrxr x'x y'y]; clear x' y' x'x y'y.
elim (xlyl xli).
clear xlyl.
intros yli xlyl.
exists yli.
apply (xLIH xli (GLeftFun y yli)).
exact xlyl.

intros yri.
left.
inversion xy as [x' y' xlyl xryr ylxl yrxr x'x y'y]; clear x' y' x'x y'y.
elim (yrxr yri).
clear yrxr.
intros xri yrxr.
exists xri.
apply (xRIH xri (GRightFun y yri)).
apply Gidentical_commutative; exact yrxr.
Qed.

Theorem GeqGlte: forall x y:Game, (Geq x y) -> (Glte x y).
Proof.
intros x y [xy yx].
exact xy.
Qed.

Theorem NGgte_Conway_Definition :
  forall x y:Game,
    Glte x y ->
    (forall xli : (GLeftIndex x), ~ Glte y (GLeftFun x xli)) /\ (forall yri : (GRightIndex y), ~ Glte (GRightFun y yri) x).
Proof.
intros x y.
intro xy; elim xy; clear x y xy.
intros until y.
intros xly xyr.
split; intro; apply NGgteIsNGgte; auto.
Qed.

Theorem NGgte_Conway_Definition2 :
  forall x y : Game,
    (forall xli : GLeftIndex  x, ~ Glte y (GLeftFun  x xli)) ->
    (forall yri : GRightIndex y, ~ Glte (GRightFun y yri) x) -> Glte x y.
Proof.
intros x y yxl yrx.
exists; intros; apply nGlteNGgte; auto.
Qed.


Inductive IsNumber : Game -> Prop :=
    IsNumber_cons :
      forall x : Game,
      (forall xli : GLeftIndex x, IsNumber (GLeftFun x xli)) ->
      (forall xri : GRightIndex x, IsNumber (GRightFun x xri)) ->
      (forall (xli : GLeftIndex x) (xri : GRightIndex x),
       NGgte (GLeftFun x xli) (GRightFun x xri)) -> 
      IsNumber x.

Lemma ZeroIsNumber : IsNumber Zero.
Proof.
exists; intro; contradiction.
Qed.

Lemma OneIsNumber : IsNumber One.
Proof.
exists; try contradiction.
intros.
apply ZeroIsNumber.
Qed.

Lemma idAntiAnti : forall x : Game, (Gidentical (AntiGame (AntiGame x)) x).
Proof.
intros.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
exists; simpl.

intro xli.
exists xli.
exact (xLIH xli).

intro xri.
exists xri.
exact (xRIH xri).

intro xli.
exists xli.
apply Gidentical_commutative.
exact (xLIH xli).

intro xri.
exists xri.
apply Gidentical_commutative.
exact (xRIH xri).
Qed.

Lemma AntiAnti : forall x : Game, Geq (AntiGame (AntiGame x)) x.
intro x; apply GidGeq.
apply idAntiAnti.
Qed.

Lemma AntiLeftIndexRight : forall x : Game, (GLeftIndex (AntiGame x)) = (GRightIndex x).
Proof.
intro x; case x; auto.
Qed.

Lemma AntiRightIndexLeft : forall x : Game, (GRightIndex (AntiGame x)) = (GLeftIndex x).
Proof.
intro x; case x; auto.
Qed.

Lemma AntiLeftFunRight : forall x : Game, (existT (fun xLI: Type => xLI -> Game) (GLeftIndex (AntiGame x))  (GLeftFun (AntiGame x))) = (existT (fun xRI: Type => xRI -> Game) (GRightIndex x) (fun xri:(GRightIndex x)=>(AntiGame (GRightFun x xri)))).
Proof.
intro x; case x; auto.
Qed.

Lemma AntiRightFunLeft : forall x : Game, (existT (fun I: Type => I -> Game) (GRightIndex (AntiGame x))  (GRightFun (AntiGame x))) = (existT (fun I: Type => I -> Game) (GLeftIndex x) (fun xri:(GLeftIndex x)=>(AntiGame (GLeftFun x xri)))).
Proof.
intro x; case x; auto.
Qed.

Lemma GlteNGgteAnti :
 forall x y : Game,
 (Glte x y -> Glte (AntiGame y) (AntiGame x)) /\
 (NGgte y x -> NGgte (AntiGame x) (AntiGame y)).
Proof.
intros x y.
eapply
 IS2Reverse
            with
            (P := 
              fun a b : Game =>
              (Glte a b -> Glte (AntiGame b) (AntiGame a)) /\
              (NGgte b a -> NGgte (AntiGame a) (AntiGame b))).
clear x y.
intros x y.
intros IHxl IHyr.
split.

intro xy.
exists.

inversion xy as [x' y' Nxly Nxyr x'x y'y]; clear x' y' x'x y'y.
cut
 (forall yri : GRightIndex y,
  NGgte x (GRightFun y yri) ->
  NGgte (AntiGame (GRightFun y yri)) (AntiGame x)).
dependent rewrite (AntiLeftFunRight y).
simpl.
apply
 Merge_quanteurs
  with
    (T := (GRightIndex y))
    (P := fun yri :(GRightIndex y) =>
          NGgte x (GRightFun y yri) ->
          NGgte (AntiGame (GRightFun y yri)) (AntiGame x))
    (Q := fun yri : (GRightIndex y) =>
          NGgte (AntiGame (GRightFun y yri)) (AntiGame x)).
intros yri IHyrGlte.
apply IHyrGlte.
apply Nxyr.

intros yri xyr.
eapply MP.
eapply proj2.
apply IHyr.

exact xyr.

inversion xy as [x' y' Nxly Nxyr x'x y'y]; clear x' y' x'x y'y.
dependent rewrite ->  (AntiRightFunLeft x); simpl.
cut
 (forall xli : (GLeftIndex x),
  let xl := GLeftFun x xli in NGgte xl y -> NGgte (AntiGame y) (AntiGame (GLeftFun x xli))).
apply
 Merge_quanteurs
  with
    (P := fun xli : GLeftIndex x =>
          let xl := GLeftFun x xli in NGgte xl y -> NGgte (AntiGame y) (AntiGame xl))
    (Q := fun xli : GLeftIndex x =>
          NGgte (AntiGame y) (AntiGame (GLeftFun x xli))).
intros xli IHxlGlte.
apply IHxlGlte.
apply Nxly.

intros.
eapply MP.
eapply proj2.
apply IHxl.

assumption.


intro xy.
cut
 ((fun x y : Game =>
   (exists r : GRightIndex x, Glte (GRightFun x r) y) \/
   (exists l : GLeftIndex y, Glte x (GLeftFun y l))) y x).
2: exact (NGgteToProp y x xy).
intros [yrx | yxl].

constructor 2.
elim yrx.
clear yrx.
intros yri yrx.
dependent rewrite ->  (AntiLeftFunRight y); simpl.
exists yri.
cut
 (forall yri : GRightIndex y,
  let yr := GRightFun y yri in Glte yr x -> Glte (AntiGame x) (AntiGame yr)).
intro IHyrGlte.
apply IHyrGlte.
exact yrx.
intros yri0 yr0.
eapply proj1.
apply IHyr with (yri := yri0).

constructor 1.
elim yxl.
clear yxl.
intros xli yxl.
dependent rewrite ->  (AntiRightFunLeft x); simpl.
exists xli.
cut
 (forall xli : GLeftIndex x,
  let xl := GLeftFun x xli in Glte y xl -> Glte (AntiGame xl) (AntiGame y)).
intro IHxlGlte.
apply IHxlGlte.
exact yxl.
intros xli0 xl0.
eapply proj1.
apply IHxl with (xli := xli0).
Qed.

Lemma GlteAnti :
 forall x y : Game, Glte x y -> Glte (AntiGame y) (AntiGame x).
intros x y.
eapply proj1.
apply GlteNGgteAnti.
Qed.

Theorem GidAnti : forall x y : Game, Gidentical x y -> Gidentical (AntiGame x) (AntiGame y).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y xy.
inversion xy as [x' y' xlyl xryr ylxl yrxr x'x y'y]; clear x' y' x'x y'y.
exists.

dependent rewrite ->  (AntiLeftFunRight x); simpl.
dependent rewrite ->  (AntiLeftFunRight y); simpl.
intro xri.
elim (xryr xri).
clear xryr.
intros yri xryr.
exists yri.
apply xRIH.
exact xryr.

dependent rewrite ->  (AntiRightFunLeft x); simpl.
dependent rewrite ->  (AntiRightFunLeft y); simpl.
intro xli.
elim (xlyl xli).
clear xlyl.
intros yli xlyl.
exists yli.
apply xLIH.
exact xlyl.

dependent rewrite ->  (AntiLeftFunRight x); simpl.
dependent rewrite ->  (AntiLeftFunRight y); simpl.
intro yri.
elim (yrxr yri).
clear yrxr.
intros xri yrxr.
exists xri.
apply Gidentical_commutative.
apply xRIH.
apply Gidentical_commutative.
exact yrxr.

dependent rewrite ->  (AntiRightFunLeft x); simpl.
dependent rewrite ->  (AntiRightFunLeft y); simpl.
intro yli.
elim (ylxl yli).
clear xlyl ylxl.
intros xli ylxl.
exists xli.
apply Gidentical_commutative.
apply xLIH.
apply Gidentical_commutative.
exact ylxl.
Qed.


Theorem GeqAnti : forall x y : Game, Geq x y -> Geq (AntiGame y) (AntiGame x).
Proof.
intros.
inversion H.
split; apply GlteAnti; assumption.
Qed.

Theorem AntiGlte :
 forall x y : Game, Glte (AntiGame y) (AntiGame x) -> Glte x y.
Proof.
intros x y AyAx.
eapply Glte_transitive.
eapply proj2; apply AntiAnti.
eapply Glte_transitive.
2: eapply proj1; apply AntiAnti.
apply GlteAnti.
exact AyAx.
Qed.

Lemma NGgteAnti :
 forall x y : Game, NGgte x y -> NGgte (AntiGame y) (AntiGame x).
intros x y.
eapply proj2.
apply GlteNGgteAnti.
Qed.

Lemma Number_AntiGame_closed :
 forall x : Game, IsNumber x -> IsNumber (AntiGame x).
intros x xIsNum.
induction x as [LI RI Lf LIH Rf RIH].
set (x := Game_cons LI RI Lf Rf) in * .
inversion xIsNum as [x' xlIsNum xrIsNum NGgtexlxr x'x]; clear x' x'x.

exists; simpl in |- * .

intro xri.
apply RIH.
apply xrIsNum.

intro xli.
apply LIH.
apply xlIsNum.

intros xri xli.
apply NGgteAnti.
apply NGgtexlxr.
Qed.

Theorem GPlusCommutative :  forall x y : Game, Gidentical (GPlus x y) (GPlus y x).
Proof.
intro x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intro y.
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
exists.


intro Pxyli.
simpl in Pxyli.
case Pxyli.

intro xli.
exists (inrT yLI _ xli).
change (GLeftFun (GPlus x y) (inlT xLI yLI xli)) with (GPlus (xLf xli) y).
change (GLeftFun (GPlus y x) (inrT yLI xLI xli)) with (GPlusAux y (xLf xli)).
rewrite <- GPlusxGPlusAux.
apply xLIH.

intro yli.
exists (inlT _ xLI yli).
change (GLeftFun (GPlus x y) (inrT xLI yLI yli)) with (GPlusAux x (yLf yli)).
change (GLeftFun (GPlus y x) (inlT yLI xLI yli)) with (GPlus (yLf yli) x).
rewrite <- GPlusxGPlusAux.
apply yLIH.


intro Pxyri.
simpl in Pxyri.
case Pxyri.

intro xri.
exists (inrT yRI _ xri).
change (GRightFun (GPlus x y) (inlT xRI yRI xri)) with (GPlus (xRf xri) y).
change (GRightFun (GPlus y x) (inrT yRI xRI xri)) with (GPlusAux y (xRf xri)).
rewrite <- GPlusxGPlusAux.
apply xRIH.

intro yri.
exists (inlT _ xRI yri).
change (GRightFun (GPlus x y) (inrT xRI yRI yri)) with (GPlusAux x (yRf yri)).
change (GRightFun (GPlus y x) (inlT yRI xRI yri)) with (GPlus (yRf yri) x).
rewrite <- GPlusxGPlusAux.
apply yRIH.


intro Pyxli.
simpl in Pyxli.
case Pyxli.

intro yli.
exists (inrT xLI _ yli).
change (GLeftFun (GPlus y x) (inlT yLI xLI yli)) with (GPlus (yLf yli) x).
change (GLeftFun (GPlus x y) (inrT xLI yLI yli)) with (GPlusAux x (yLf yli)).
rewrite <- GPlusxGPlusAux.
apply Gidentical_commutative.
apply yLIH.

intro xli.
exists (inlT _ yLI xli).
change (GLeftFun (GPlus y x) (inrT yLI xLI xli)) with (GPlusAux y (xLf xli)).
change (GLeftFun (GPlus x y) (inlT xLI yLI xli)) with (GPlus (xLf xli) y).
rewrite <- GPlusxGPlusAux.
apply Gidentical_commutative.
apply xLIH.


intro Pyxri.
simpl in Pyxri.
case Pyxri.

intro yri.
exists (inrT xRI _ yri).
change (GRightFun (GPlus y x) (inlT yRI xRI yri)) with (GPlus (yRf yri) x).
change (GRightFun (GPlus x y) (inrT xRI yRI yri)) with (GPlusAux x (yRf yri)).
rewrite <- GPlusxGPlusAux.
apply Gidentical_commutative.
apply yRIH.

intro xri.
exists (inlT _ yRI xri).
change (GRightFun (GPlus y x) (inrT yRI xRI xri)) with (GPlusAux y (xRf xri)).
change (GRightFun (GPlus x y) (inlT xRI yRI xri)) with (GPlus (xRf xri) y).
rewrite <- GPlusxGPlusAux.
apply Gidentical_commutative.
apply xRIH.
Qed.

Theorem GPlusCommutativeGeq : forall x y : Game, Geq (GPlus x y) (GPlus y x).
Proof.
intros x y.
apply GidGeq; apply GPlusCommutative.
Qed.


Theorem GPlusCommutativeGlte :
 forall x y : Game, Glte (GPlus x y) (GPlus y x).
Proof.
intros x y.
apply GidGlte.
apply GPlusCommutative.
Qed.

Require Relation_Definitions.
Require Setoid.

Lemma GameId_SetoidTheory : Setoid.Setoid_Theory Game Gidentical.
Proof.
exists.

exact Gidentical_reflexive.

intros x y; apply Gidentical_commutative.

exact Gidentical_transitive.
Qed.

Add Setoid  Game Gidentical (GameId_SetoidTheory) as GameId_Setoid.

Lemma Glte_trs: forall x y z: Game, Glte x y -> Glte y z -> Glte x z.
Proof.
intros until z; apply Glte_transitive; assumption.
Qed.

Add Relation Game Glte
reflexivity  proved by Glte_reflexive
transitivity proved by Glte_trs
as Glte_rel.

Lemma GameEq_SetoidTheory : Setoid.Setoid_Theory Game Geq.
Proof.
exists.

exact Geq_reflexive.

exact Geq_symmetric.

exact Geq_transitive.
Qed.

Add Setoid Game Geq GameEq_SetoidTheory as GameEq_Setoid.

Add Morphism Glte with signature Gidentical ==> Gidentical ==> Setoid.impl as Glte_MorphId.
Proof.
intros x x' xx' y y' yy' xy.
eapply Glte_transitive.
apply (GidGlte x' x (Gidentical_commutative x' x xx')).
eapply Glte_transitive.
apply xy.
apply GidGlte; assumption.
Qed.

Add Morphism Glte with signature Geq ==> Geq ==> Setoid.impl as Glte_MorphEq.
Proof.
intros x x' [xx' x'x] y y' [yy' y'y] xy.
rewrite -> x'x.
rewrite <- yy'.
exact xy.
Qed.

Add Morphism Geq with signature Gidentical ==> Gidentical ==> iff as Geq_MorphId.
intros x x' xx' y y' yy'.
split.

intros [ xy yx ].
split; rewrite <-  xx'; rewrite <-  yy'; assumption.

intros [ x'y' y'x' ].
split; rewrite -> xx'; rewrite -> yy'; assumption.
Qed.

Lemma GLeftIndexGPlus: forall x y:Game, (GLeftIndex (GPlus x y)) = (sumT (GLeftIndex x) (GLeftIndex y)).
Proof.
intros x y.
case x.
intros xLI xRI xLf xRf.
case y.
intros yLI yRI yLf yRf.
clear x y.
reflexivity.
Qed.

Lemma GRightIndexGPlus: forall x y:Game, (GRightIndex (GPlus x y)) = (sumT (GRightIndex x) (GRightIndex y)).
Proof.
intros x y.
case x.
intros xLI xRI xLf xRf.
case y.
intros yLI yRI yLf yRf.
clear x y.
reflexivity.
Qed.

Lemma GLeftFunGPlus : forall x y: Game, (existT (fun T: Type => T -> Game) (GLeftIndex (GPlus x y))  (GLeftFun (GPlus x y))) = (existT (fun T: Type => T -> Game) (sumT (GLeftIndex x) (GLeftIndex y))
     (map_on_sumT (GLeftIndex x) (GLeftIndex y) Game
        (fun xli : (GLeftIndex x) => GPlus (GLeftFun x xli) y)
        (fun yli : (GLeftIndex y) => GPlusAux x (GLeftFun y yli)))).
Proof.
intro x; case x; intros until y; case y; progress auto.
Qed.

Lemma GRightFunGPlus : forall x y: Game, (existT (fun T: Type => T -> Game) (GRightIndex (GPlus x y))  (GRightFun (GPlus x y))) = (existT (fun T: Type => T -> Game) (sumT (GRightIndex x) (GRightIndex y))
     (map_on_sumT (GRightIndex x) (GRightIndex y) Game
        (fun xli : (GRightIndex x) => GPlus (GRightFun x xli) y)
        (fun yli : (GRightIndex y) => GPlusAux x (GRightFun y yli)))).
Proof.
intro x; case x; intros until y; case y; progress auto.
Qed.

Add Morphism GPlus with signature Gidentical ==> Gidentical ==> Gidentical as GPlus_MorphId.
Proof.
intro w.
induction w as [wLI wRI wLf wLIH wRf wRIH].
set (w := Game_cons wLI wRI wLf wRf) in |- * .
intros x wx y.
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
intros z.
intros yz.
inversion wx as [w' x' wlxl wrxr xlwl xrwr w'w x'x]; clear w' x' w'w x'x.
inversion yz as [y' z' ylzl yrzr zlyl zryr y'y z'z]; clear y' z' y'y z'z.
exists.


clear wrxr xrwr yrzr zryr.
dependent rewrite ->  (GLeftFunGPlus w y); simpl.
intro Pwyli.
case Pwyli; simpl.

intro wli; clear Pwyli.
simpl.
elim (wlxl wli).
clear wlxl xlwl.
intros xli wlxl.
dependent rewrite ->  (GLeftFunGPlus x z); simpl.
exists (inlT (GLeftIndex x) (GLeftIndex z) xli).
simpl.
apply wLIH; assumption.

intro yli; clear Pwyli.
elim (ylzl yli).
clear ylzl ylzl.
intros zli ylzl.
dependent rewrite ->  (GLeftFunGPlus x z); simpl.
exists (inrT (GLeftIndex x) (GLeftIndex z) zli).
simpl.
rewrite <- (GPlusxGPlusAux w).
rewrite <- (GPlusxGPlusAux x).
apply yLIH; assumption.


clear wlxl xlwl ylzl zlyl.
dependent rewrite ->  (GLeftFunGPlus w y); simpl.
intro Pwyri.
case Pwyri; simpl.

intro wri; clear Pwyri.
simpl.
elim (wrxr wri).
clear wrxr xrwr.
intros xri wrxr.
dependent rewrite ->  (GRightFunGPlus x z); simpl.
exists (inlT (GRightIndex x) (GRightIndex z) xri).
simpl.
apply wRIH; assumption.

intro yri; clear Pwyri.
elim (yrzr yri).
clear yrzr yrzr.
intros zri yrzr.
dependent rewrite ->  (GRightFunGPlus x z); simpl.
exists (inrT (GRightIndex x) (GRightIndex z) zri).
simpl.
rewrite <- (GPlusxGPlusAux w).
rewrite <- (GPlusxGPlusAux x).
apply yRIH; assumption.


clear wrxr xrwr yrzr zryr.
dependent rewrite ->  (GLeftFunGPlus x z); simpl.
intro Pxzli.
case Pxzli; simpl.

intro xli; clear Pxzli.
simpl.
elim (xlwl xli).
clear wlxl xlwl.
intros wli xlwl.
exists (inlT (GLeftIndex w) (GLeftIndex y) wli).
simpl.
apply Gidentical_commutative.
apply wLIH; try assumption; apply Gidentical_commutative; assumption.

intro zli; clear Pxzli.
elim (zlyl zli).
clear zlyl zlyl.
intros yli zlyl.
exists (inrT (GLeftIndex w) (GLeftIndex y) yli).
simpl.
rewrite <- (GPlusxGPlusAux w).
rewrite <- (GPlusxGPlusAux x).
apply Gidentical_commutative.
apply yLIH; try assumption; apply Gidentical_commutative; assumption.


clear wlxl xlwl ylzl zlyl.
dependent rewrite ->  (GRightFunGPlus x z); simpl.
intro Pxzri.
case Pxzri; simpl.

intro xri; clear Pxzri.
simpl.
elim (xrwr xri).
clear wrxr xrwr.
intros wri xrwr.
exists (inlT (GRightIndex w) (GRightIndex y) wri).
simpl.
apply Gidentical_commutative.
apply wRIH; try assumption; apply Gidentical_commutative; assumption.

intro zri; clear Pxzri.
elim (zryr zri).
clear yrzr yrzr zryr.
intros yri zryr.
exists (inrT (GRightIndex w) (GRightIndex y) yri).
simpl.
rewrite <- (GPlusxGPlusAux w).
rewrite <- (GPlusxGPlusAux x).
apply Gidentical_commutative.
apply yRIH; try assumption; apply Gidentical_commutative; assumption.
Qed.

Theorem GPlusOrder :
 forall x y z : Game,
 (Glte x y -> Glte (GPlus x z) (GPlus y z)) /\
 (NGgte x y -> NGgte (GPlus x z) (GPlus y z)).
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y.
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
intros z.
induction z as [zLI zRI zLf zLIH zRf zRIH].
set (z := Game_cons zLI zRI zLf zRf) in |- * .

split.

intro xy.
inversion xy as [x' y' xly xyr x'x y'y]; clear x' y' x'x y'y.

exists.

intros xzli.
simpl in xzli.
dependent rewrite ->  (GLeftFunGPlus y z); simpl.

case xzli; [ intros xli | intros zli ].
change (GLeftFun (GPlus x z) (inlT xLI zLI xli)) with (GPlus (xLf xli) z).
2: change (GLeftFun (GPlus x z) (inrT xLI zLI zli)) with (GPlusAux x (zLf zli)).
eapply MP;
 [ eapply proj2; apply xLIH with (l := xli) (y := y) (z := z) | apply xly ].
constructor 2; exists (inrT yLI zLI zli).
simpl.
change (Glte (GPlusAux x (zLf zli)) (GPlusAux y (zLf zli))).
rewrite <- GPlusxGPlusAux with (x := x) (y := zLf zli).
rewrite <- GPlusxGPlusAux with (x := y) (y := zLf zli).
eapply MP; [ eapply proj1; apply zLIH with (l := zli) | apply xy ].


intros yzri.

case yzri; [ intros yri | intros zri ].
eapply MP; [ eapply proj2; apply yRIH with (r := yri) (z := z) | apply xyr ].
constructor 1. exists (inrT xRI zRI zri).
change (Glte (GPlusAux x (GRightFun z zri)) (GPlusAux y (GRightFun z zri))).
rewrite <- (GPlusxGPlusAux x (GRightFun z zri)).
rewrite <- (GPlusxGPlusAux y (GRightFun z zri)).
eapply MP; [ eapply proj1; apply zRIH with (r := zri) | apply xy ].




intro xy.
inversion xy as [x' y' xry x'x y'y | x' y' xyl x'x y'y]; clear x' y' x'x y'y.
elim xry.
clear xry.
intros xri xry.
constructor 1.
exists (inlT xRI zRI xri).
eapply MP. eapply proj1; apply xRIH with (r := xri) (y := y) (z := z).
exact xry.

elim xyl.
clear xyl.
intros yli xyl.
constructor 2.
exists (inlT yLI zLI yli).
eapply MP. eapply proj1; apply yLIH with (l := yli) (z := z).
exact xyl.
Qed.

Add Morphism NGgte with signature Gidentical ==> Gidentical ==> Setoid.impl as NGgte_MorphId.
Proof.
intros x x' xx' y y' yy' xy.
inversion xy as [x0 y0 ExrNGxry x0x y0y | x0 y0 EylNGxyl x0x y0y]; clear x0 y0 x0x y0y.

left.
elim ExrNGxry.
intros xri xry.
inversion xx' as [x0 x'0 xlx'l xrx'r x'lxl x'rxr x0x x'0x']; clear x0 x'0 x0x x'0x'.
elim (xrx'r xri); clear xrx'r.
intros x'ri xrx'r.
exists x'ri.
rewrite <- yy'.
rewrite <- xrx'r.
assumption.

right.
elim EylNGxyl.
intros yli xyl.
inversion yy' as [y0 y'0 yly'l yry'r y'lyl y'ryr y0y y'0y']; clear y0 y'0 y0y y'0y'.
elim (yly'l yli); clear yly'l.
intros y'li yly'l.
exists y'li.
rewrite <- xx'.
rewrite <- yly'l.
assumption.
Qed.

Add Morphism GPlus with signature Glte ++> eq ==> Glte as GPlusGlteLeft.
Proof.
intros x y.
apply raise_quantifier with
  (T:=Game)
  (P:= Glte x y)
  (Q:= fun z : Game => Glte (GPlus x z) (GPlus y z)).
intros z. 
eapply proj1.
apply GPlusOrder.
Qed.

Add Morphism GPlus with signature eq ==> Glte ++> Glte as GPlusGlteRight.
intros z x y.
intro xy.
setoid_rewrite -> (GPlusCommutative z x).
setoid_rewrite -> (GPlusCommutative z y).
apply GPlusGlteLeft.
assumption.
Qed.

Add Morphism GPlus with signature Glte ++> Glte ++> Glte as GPlusGlteBoth.
Proof.
intros x x' xx' y y' yy'.
eapply Glte_transitive.
apply GPlusGlteRight.
apply yy'.
apply GPlusGlteLeft.
apply xx'.
Qed.

Add Relation Game NGgte as NGgte_rel.

Add Morphism GPlus with signature NGgte ++> eq ==> NGgte as GPlusNGgteLeft.
Proof.
intros x y.
apply raise_quantifier with
  (T:=Game)
  (P:= NGgte x y)
  (Q:= fun z : Game => NGgte (GPlus x z) (GPlus y z)).
intros z.
eapply proj2.
apply GPlusOrder.
Qed.

Add Morphism GPlus with signature NGgte ++> NGgte as GPlusNGgteRight.
Proof.
intros z x y xy.
rewrite <- (GPlusCommutative x z).
rewrite <- (GPlusCommutative y z).
apply GPlusNGgteLeft.
assumption.
Qed.

Add Morphism GPlus with signature Geq ==> Geq ==> Geq as GPlusGeqBoth.
intros x x' [ xx' x'x ] y y' [ yy' y'y].
split; apply GPlusGlteBoth; assumption.
Qed.

Add Morphism GPlus with signature Geq ==> Geq as GPlusGeqRight.
intros x y y' [ yy' y'y].
split; apply GPlusGlteRight; assumption.
Qed.

Add Morphism GPlus with signature Geq ==> eq ==> Geq as GPlusGeqLeft.
intros x x' [ xx' x'x] y.
split; apply GPlusGlteLeft; assumption.
Qed.

Add Morphism AntiGame with signature Gidentical ==> Gidentical as GAnti_MorphId.
exact GidAnti.
Qed.

Add Morphism AntiGame with signature Glte --> Glte as GAnti_MorphGlte.
intros x y; apply GlteAnti.
Qed.

Add Morphism AntiGame with signature Geq ==> Geq as GAnti_MorphEq.
intros x y [ xy yx ].
split; apply GAnti_MorphGlte; assumption.
Qed.

Theorem GPlusAssociative :
 forall x y z : Game, Gidentical (GPlus x (GPlus y z)) (GPlus (GPlus x y) z).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y.
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
intros z.
induction z as [zLI zRI zLf zLIH zRf zRIH].
set (z := Game_cons zLI zRI zLf zRf) in |- * .
exists.


intros PxPyzli.
simpl in PxPyzli.
case PxPyzli; clear PxPyzli.

intros xli.
exists (inlT _ (GLeftIndex z) (inlT xLI (GLeftIndex y) xli)).
apply (xLIH xli y z).

intros Pyzli.
case Pyzli; clear Pyzli.
intro yli; simpl in yli.
exists (inlT _ (GLeftIndex z) (inrT xLI (GLeftIndex y) yli)).
change (Gidentical (GPlusAux x (GPlus (GLeftFun y yli) z)) (GPlus (GPlusAux x (GLeftFun y yli)) z)).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux x).
apply yLIH.
intro zli; simpl in zli.
exists (inrT (sumT xLI (GLeftIndex y)) (GLeftIndex z) zli).
change (Gidentical (GPlusAux x (GPlusAux y (GLeftFun z zli))) (GPlusAux (GPlusAux x y) (GLeftFun z zli))).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux y).
rewrite <- (GPlusxGPlusAux (GPlus x y)).
apply zLIH.


intros PxPyzri.
simpl in PxPyzri.
case PxPyzri; clear PxPyzri.

intros xri.
exists (inlT _ (GRightIndex z) (inlT xRI (GRightIndex y) xri)).
apply (xRIH xri y z).

intros Pyzri.
case Pyzri; clear Pyzri.
intro yri; simpl in yri.
exists (inlT _ (GRightIndex z) (inrT xRI (GRightIndex y) yri)).
change (Gidentical (GPlusAux x (GPlus (GRightFun y yri) z)) (GPlus (GPlusAux x (GRightFun y yri)) z)).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux x).
apply yRIH.
intro zri; simpl in zri.
exists (inrT (sumT xRI (GRightIndex y)) (GRightIndex z) zri).
change (Gidentical (GPlusAux x (GPlusAux y (GRightFun z zri))) (GPlusAux (GPlusAux x y) (GRightFun z zri))).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux y).
rewrite <- (GPlusxGPlusAux (GPlus x y)).
apply zRIH.


intros PPxyzli.
simpl in PPxyzli.
case PPxyzli; clear PPxyzli.

intros Pxyli.
case Pxyli; clear Pxyli.
intro xli; simpl in xli.
exists (inlT _ (sumT yLI (GLeftIndex z)) xli).
change (Gidentical (GPlus (GPlus (xLf xli) y) z) (GPlus (xLf xli) (GPlus y z))).
apply Gidentical_commutative; apply (xLIH xli y z).
intro yli; simpl in yli.
exists (inrT xLI (sumT (GLeftIndex y) (GLeftIndex z)) (inlT (GLeftIndex y) (GLeftIndex z) yli)).
change (Gidentical (GPlus (GPlusAux x (GLeftFun y yli)) z) (GPlusAux x (GPlus (GLeftFun y yli) z))).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux x).
apply Gidentical_commutative; apply (yLIH yli z).

intros zli.
exists (inrT xLI _ (inrT yLI (GLeftIndex z) zli)).
change (Gidentical (GPlusAux (GPlus x y) (zLf zli)) (GPlusAux x (GPlusAux y (zLf zli)))).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux y).
rewrite <- (GPlusxGPlusAux (GPlus x y)).
apply Gidentical_commutative; apply (zLIH zli).


intros PPxyzri.
simpl in PPxyzri.
case PPxyzri; clear PPxyzri.

intros Pxyri.
case Pxyri; clear Pxyri.
intro xri; simpl in xri.
exists (inlT (GRightIndex x) (GRightIndex (GPlus y z)) xri).
change (Gidentical (GPlus (GPlus (GRightFun x xri) y) z) (GPlus (GRightFun x xri) (GPlus y z))).
apply Gidentical_commutative; apply (xRIH xri y z).
intro yri; simpl in yri.
exists (inrT xRI (sumT (GRightIndex y) (GRightIndex z)) (inlT (GRightIndex y) (GRightIndex z) yri)).
change (Gidentical (GPlus (GPlusAux x (GRightFun y yri)) z) (GPlusAux x (GPlus (GRightFun y yri) z))).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux x).
apply Gidentical_commutative; apply yRIH.

intros zri.
exists (inrT (GRightIndex x) _ (inrT (GRightIndex y) (GRightIndex z) zri)).
change (Gidentical (GPlusAux (GPlus x y) (GRightFun z zri)) (GPlusAux x (GPlusAux y (GRightFun z zri)))).
rewrite <- (GPlusxGPlusAux x).
rewrite <- (GPlusxGPlusAux y).
rewrite <- (GPlusxGPlusAux (GPlus x y)).
apply Gidentical_commutative; apply (zRIH zri).
Qed.

Theorem GPlusAssociative_Glte :
 forall x y z : Game, Glte (GPlus x (GPlus y z)) (GPlus (GPlus x y) z).
Proof.
intros.
apply GidGlte.
apply GPlusAssociative.
Qed.

Theorem GPlusAssociative_Geq :
 forall x y z : Game, Geq (GPlus x (GPlus y z)) (GPlus (GPlus x y) z).
Proof.
intros.
apply GidGeq.
apply GPlusAssociative.
Qed.

Theorem AntiGPlus :
 forall x y : Game,
 Gidentical (AntiGame (GPlus x y)) (GPlus (AntiGame x) (AntiGame y)).
Proof.
intro x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intro y.
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
exists.


intro APxyli.
simpl in APxyli.
case APxyli; clear APxyli.

intro xri.
exists (inlT xRI yRI xri).
change (Gidentical (AntiGame (GPlus (xRf xri) y)) (GPlus (AntiGame (xRf xri)) (AntiGame y))).
apply xRIH.

intro yri.
exists (inrT xRI yRI yri).
change (Gidentical (AntiGame (GPlusAux x (GRightFun y yri))) (GPlusAux (AntiGame x) (AntiGame (GRightFun y yri)))).
rewrite <- GPlusxGPlusAux.
rewrite <- GPlusxGPlusAux.
apply yRIH.


intro APxyri.
simpl in APxyri.
case APxyri; clear APxyri.

intro xli.
exists (inlT xLI yLI xli).
change (Gidentical (AntiGame (GPlus (GLeftFun x xli) y)) (GPlus (AntiGame (xLf xli)) (AntiGame y))).
apply xLIH.

intro yli.
exists (inrT xLI yLI yli).
change (Gidentical (AntiGame (GPlusAux x (yLf yli))) (GPlusAux (AntiGame x) (AntiGame (yLf yli)))).
rewrite <- GPlusxGPlusAux.
rewrite <- GPlusxGPlusAux.
apply yLIH.


intro PAxAyli.
simpl in PAxAyli.
case PAxAyli; clear PAxAyli.

intro xri.
exists (inlT _ yRI xri).
change (Gidentical (GPlus (AntiGame (xRf xri)) (AntiGame y)) (AntiGame (GPlus (xRf xri) y))).
apply Gidentical_commutative.
apply xRIH.

intro yri.
exists (inrT xRI _ yri).
change (Gidentical (GPlusAux (AntiGame x) (AntiGame (yRf yri))) (AntiGame (GPlusAux x (yRf yri)))).
apply Gidentical_commutative.
rewrite <- GPlusxGPlusAux.
rewrite <- GPlusxGPlusAux.
apply yRIH.


intro PAxAyri.
simpl in PAxAyri.
case PAxAyri; clear PAxAyri.

intro xli.
exists (inlT _ yLI xli).
change (Gidentical (GPlus (AntiGame (GLeftFun x xli)) (AntiGame y)) (AntiGame (GPlus (GLeftFun x xli) y))).
apply Gidentical_commutative.
apply xLIH.

intro yli.
exists (inrT xLI _ yli).
change (Gidentical (GPlusAux (AntiGame x) (AntiGame (GLeftFun y yli))) (AntiGame (GPlusAux x (GLeftFun y yli)))).
rewrite <- GPlusxGPlusAux.
rewrite <- GPlusxGPlusAux.
apply Gidentical_commutative.
apply yLIH.
Qed.

Theorem AntiGPlus_Glte :
 forall x y : Game,
 Glte (AntiGame (GPlus x y)) (GPlus (AntiGame x) (AntiGame y)).
Proof.
intros.
apply GidGlte.
apply AntiGPlus.
Qed.

Theorem AntiGPlus_Glte2 :
 forall x y : Game,
 Glte (GPlus (AntiGame x) (AntiGame y)) (AntiGame (GPlus x y)).
Proof.
intros.
apply GidGlte.
apply Gidentical_commutative.
apply AntiGPlus.
Qed.

Theorem AntiGPlus_Geq :
 forall x y : Game,
 Geq (AntiGame (GPlus x y)) (GPlus (AntiGame x) (AntiGame y)).
Proof.
intros.
apply GidGeq.
apply AntiGPlus.
Qed.

Theorem xPlusAntixZero_one :
 forall x : Game, Glte (GPlus x (AntiGame x)) Zero.
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in * .
exists.
2: intro; contradiction.
intro xi; simpl in xi; case xi; [ intro xli | intro xri ]; clear xi.

change (NGgte (GPlus (xLf xli) (AntiGame x)) Zero).
left.
dependent rewrite -> (GRightFunGPlus (xLf xli) (AntiGame x)).
simpl.
exists (inrT (GRightIndex (xLf xli)) xLI xli).
simpl.
rewrite <- (GPlusxGPlusAux (xLf xli)).
exact (xLIH xli).

change (NGgte (GPlusAux x (AntiGame (xRf xri))) Zero).
rewrite <- GPlusxGPlusAux.
left.
dependent rewrite -> (GRightFunGPlus x (AntiGame (xRf xri))).
simpl.
exists (inlT xRI (GRightIndex (AntiGame (xRf xri))) xri).
simpl.
exact (xRIH xri).
Qed.

Theorem xPlusAntixZero : forall x : Game, Geq (GPlus x (AntiGame x)) Zero.
Proof.
intros; split.
apply xPlusAntixZero_one.
apply AntiGlte.
rewrite -> AntiGPlus.
eapply Glte_transitive with (y := Zero).
apply xPlusAntixZero_one.
exists; intro; contradiction.
Qed.

Theorem AntixPlusxZero : forall x : Game, Geq (GPlus (AntiGame x) x) Zero.
Proof.
intros.
rewrite -> (GPlusCommutative (AntiGame x) x).
apply xPlusAntixZero.
Qed.

Lemma GidxGPlusxZero : forall x : Game, Gidentical x (GPlus x Zero).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in * .
exists.

intro xli.
dependent rewrite -> (GLeftFunGPlus x Zero).
simpl.
exists (inlT (GLeftIndex x) (GLeftIndex Zero) xli).
simpl.
apply (xLIH xli).

intro xri.
dependent rewrite -> (GRightFunGPlus x Zero).
simpl.
exists (inlT (GRightIndex x) (GRightIndex Zero) xri).
simpl.
apply (xRIH xri).

intros PxZli.
simpl in PxZli; case PxZli; clear PxZli.
2: intro; contradiction.
intro xli; exists xli.
simpl.
apply Gidentical_commutative; apply xLIH.

intros PxZri.
simpl in PxZri; case PxZri; clear PxZri.
2: intro; contradiction.
intro xri; exists xri.
simpl.
apply Gidentical_commutative; apply xRIH.
Qed.

Lemma GidxGPlusZerox : forall x : Game, Gidentical x (GPlus Zero x).
Proof.
intros x.
rewrite -> GPlusCommutative.
apply GidxGPlusxZero.
Qed.

Lemma GltexGPlusxZero : forall x : Game, Glte x (GPlus x Zero).
Proof.
intros.
apply GidGlte.
apply GidxGPlusxZero.
Qed.

Lemma GltexGPlusZerox : forall x : Game, Glte x (GPlus Zero x).
Proof.
intros.
apply GidGlte.
apply GidxGPlusZerox.
Qed.

Lemma GlteGPlusxZerox : forall x : Game, Glte (GPlus x Zero) x.
Proof.
intros.
apply GidGlte.
apply Gidentical_commutative.
apply GidxGPlusxZero.
Qed.

Lemma GlteGPlusZeroxx : forall x : Game, Glte (GPlus Zero x) x.
Proof.
intros.
apply GidGlte.
apply Gidentical_commutative.
rewrite -> GPlusCommutative.
apply GidxGPlusxZero.
Qed.

(***** We now have "(No, +) is a commutative group" *****)

Fixpoint GMult (x y : Game) {struct x} : Game :=
  let GMultAux :=
    (fix GMultAux (z : Game) : Game := (* (GPlusAux) == (GPlus x) *)
      Game_cons
        (sumT (GMult_prodT (GLeftIndex x) (GLeftIndex z)) (GMult_prodT (GRightIndex x) (GRightIndex z)))
        (sumT (GMult_prodT (GLeftIndex x) (GRightIndex z)) (GMult_prodT (GRightIndex x) (GLeftIndex z)))
	(map_on_sumT (GMult_prodT (GLeftIndex x) (GLeftIndex z)) (GMult_prodT (GRightIndex x) (GRightIndex z)) Game
	  (fun lli : GMult_prodT (GLeftIndex x) (GLeftIndex z) =>
            let (xli, zli) := lli in
            let xl := GLeftFun x xli in
            let zl := GLeftFun z zli in
              GPlus (GPlus (GMult xl z) (GMultAux zl)) (AntiGame (GMult xl zl)))
	  (fun rri : GMult_prodT (GRightIndex x) (GRightIndex z) =>
            let (xri, zri) := rri in
            let xr := GRightFun x xri in
            let zr := GRightFun z zri in
              GPlus (GPlus (GMult xr z) (GMultAux zr)) (AntiGame (GMult xr zr))))
	(map_on_sumT (GMult_prodT (GLeftIndex x) (GRightIndex z)) (GMult_prodT (GRightIndex x) (GLeftIndex z)) Game
	  (fun lri : GMult_prodT (GLeftIndex x) (GRightIndex z) =>
            let (xli, zri) := lri in
            let xl := GLeftFun x xli in
            let zr := GRightFun z zri in
              GPlus (GPlus (GMult xl z) (GMultAux zr)) (AntiGame (GMult xl zr)))
	  (fun rli : GMult_prodT (GRightIndex x) (GLeftIndex z) =>
            let (xri, zli) := rli in
            let xr := GRightFun x xri in
	    let zl := GLeftFun z zli in
	      GPlus (GPlus (GMult xr z) (GMultAux zl)) (AntiGame (GMult xr zl))))) in
    (GMultAux y).

Definition GMultAux (x : Game) :=
    (fix GMultAux (z : Game) : Game := (* (GPlusAux) == (GPlus x) *)
      Game_cons
        (sumT (GMult_prodT (GLeftIndex x) (GLeftIndex z)) (GMult_prodT (GRightIndex x) (GRightIndex z)))
        (sumT (GMult_prodT (GLeftIndex x) (GRightIndex z)) (GMult_prodT (GRightIndex x) (GLeftIndex z)))
	(map_on_sumT (GMult_prodT (GLeftIndex x) (GLeftIndex z)) (GMult_prodT (GRightIndex x) (GRightIndex z)) Game
	  (fun lli : GMult_prodT (GLeftIndex x) (GLeftIndex z) =>
            let (xli, zli) := lli in
            let xl := GLeftFun x xli in
            let zl := GLeftFun z zli in
              GPlus (GPlus (GMult xl z) (GMultAux zl)) (AntiGame (GMult xl zl)))
	  (fun rri : GMult_prodT (GRightIndex x) (GRightIndex z) =>
            let (xri, zri) := rri in
            let xr := GRightFun x xri in
            let zr := GRightFun z zri in
              GPlus (GPlus (GMult xr z) (GMultAux zr)) (AntiGame (GMult xr zr))))
	(map_on_sumT (GMult_prodT (GLeftIndex x) (GRightIndex z)) (GMult_prodT (GRightIndex x) (GLeftIndex z)) Game
	  (fun lri : GMult_prodT (GLeftIndex x) (GRightIndex z) =>
            let (xli, zri) := lri in
            let xl := GLeftFun x xli in
            let zr := GRightFun z zri in
              GPlus (GPlus (GMult xl z) (GMultAux zr)) (AntiGame (GMult xl zr)))
	  (fun rli : GMult_prodT (GRightIndex x) (GLeftIndex z) =>
            let (xri, zli) := rli in
            let xr := GRightFun x xri in
	    let zl := GLeftFun z zli in
	      GPlus (GPlus (GMult xr z) (GMultAux zl)) (AntiGame (GMult xr zl))))).

Lemma GMultxGMultAux : forall x y : Game, (GMult x y) = (GMultAux x y).
Proof.
intros [xLI xRI xLf xRf] [yLI yRI yLf yRf].
set (x := Game_cons xLI xRI xLf xRf) in * .
set (y := Game_cons yLI yRI yLf yRf) in * .
reflexivity.
Qed.

Lemma GidGMultxZeroZero : forall x : Game, Gidentical (GMult x Zero) Zero.
Proof.
intros x.
case x; intros xLI xRI xLf xRf.
clear x; set (x := Game_cons xLI xRI xLf xRf) in * .
exists.

intro MxZli.
case MxZli; intro p; case p; contradiction.

intro MxZri.
case MxZri; intro p; case p; contradiction.

intro Zli; simpl in Zli; contradiction.

intro Zri; simpl in Zri; contradiction.
Qed.

Theorem GlteGMultxZeroZero : forall x : Game, Glte (GMult x Zero) Zero.
intros x.
apply GidGlte.
apply GidGMultxZeroZero.
Qed.

Theorem GlteZeroGMultxZero : forall x : Game, Glte Zero (GMult x Zero).
intros x.
apply GidGlte.
apply Gidentical_commutative.
apply GidGMultxZeroZero.
Qed.

Theorem GMultCommutative : forall x y : Game, Gidentical (GMult x y) (GMult y x).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in * .
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in * .
exists.


intro Mxyli; simpl in Mxyli.
case Mxyli; clear Mxyli.

intros [xli yli].
exists (inlT   _ (GMult_prodT yRI xRI) (GMult_pairT yli xli)).
change (Gidentical (GPlus (GPlus (GMult (xLf xli) y) (GMultAux x (yLf yli))) (AntiGame (GMult (xLf xli) (yLf yli))))
                   (GPlus (GPlus (GMult (yLf yli) x) (GMultAux y (xLf xli))) (AntiGame (GMult (yLf yli) (xLf xli))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (xLIH xli y).
rewrite -> (yLIH yli).
rewrite -> (GPlusCommutative (GMult y (xLf xli))).
rewrite -> (xLIH xli (yLf yli)).
reflexivity.

intros [xri yri].
exists (inrT (GMult_prodT yLI xLI) (GMult_prodT yRI xRI) (GMult_pairT yri xri)).
change (Gidentical (GPlus (GPlus (GMult (xRf xri) y) (GMultAux x (yRf yri))) (AntiGame (GMult (xRf xri) (yRf yri))))
                   (GPlus (GPlus (GMult (yRf yri) x) (GMultAux y (xRf xri))) (AntiGame (GMult (yRf yri) (xRf xri))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (xRIH xri y).
rewrite -> (yRIH yri).
rewrite -> (GPlusCommutative (GMult y (xRf xri))).
rewrite -> (xRIH xri (yRf yri)).
reflexivity.


intro Mxyri; simpl in Mxyri.
case Mxyri; clear Mxyri.

intros [xli yri].
exists (inrT (GMult_prodT yLI xRI) (GMult_prodT yRI xLI) (GMult_pairT yri xli)).
change (Gidentical (GPlus (GPlus (GMult (xLf xli) y) (GMultAux x (yRf yri))) (AntiGame (GMult (xLf xli) (yRf yri))))
                   (GPlus (GPlus (GMult (yRf yri) x) (GMultAux y (xLf xli))) (AntiGame (GMult (yRf yri) (xLf xli))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (xLIH xli y).
rewrite -> (yRIH yri).
rewrite -> (GPlusCommutative (GMult y (xLf xli))).
rewrite -> (xLIH xli (yRf yri)).
reflexivity.

intros [xri yli].
exists (inlT (GMult_prodT yLI xRI) (GMult_prodT yRI xLI) (GMult_pairT yli xri)).
change (Gidentical (GPlus (GPlus (GMult (xRf xri) y) (GMultAux x (yLf yli))) (AntiGame (GMult (xRf xri) (yLf yli))))
                   (GPlus (GPlus (GMult (yLf yli) x) (GMultAux y (xRf xri))) (AntiGame (GMult (yLf yli) (xRf xri))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (xRIH xri y).
rewrite -> (yLIH yli).
rewrite -> (GPlusCommutative (GMult y (xRf xri))).
rewrite -> (xRIH xri (yLf yli)).
reflexivity.


intro Myxli; simpl in Myxli.
case Myxli; clear Myxli.

intros [yli xli].
exists (inlT   _ (GMult_prodT xRI yRI) (GMult_pairT xli yli)).
change (Gidentical (GPlus (GPlus (GMult (yLf yli) x) (GMultAux y (xLf xli))) (AntiGame (GMult (yLf yli) (xLf xli))))
                   (GPlus (GPlus (GMult (xLf xli) y) (GMultAux x (yLf yli))) (AntiGame (GMult (xLf xli) (yLf yli))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (yLIH yli).
rewrite -> (xLIH xli).
rewrite -> (GPlusCommutative (GMult y (xLf xli))).
rewrite -> (xLIH xli (yLf yli)).
reflexivity.

intros [yri xri].
exists (inrT (GMult_prodT xLI yLI) (GMult_prodT xRI yRI) (GMult_pairT xri yri)).
change (Gidentical (GPlus (GPlus (GMult (yRf yri) x) (GMultAux y (xRf xri))) (AntiGame (GMult (yRf yri) (xRf xri))))
                   (GPlus (GPlus (GMult (xRf xri) y) (GMultAux x (yRf yri))) (AntiGame (GMult (xRf xri) (yRf yri))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (yRIH yri).
rewrite -> (xRIH xri).
rewrite -> (GPlusCommutative (GMult y (xRf xri))).
rewrite -> (xRIH xri (yRf yri)).
reflexivity.


intro Myxri; simpl in Myxri.
case Myxri; clear Myxri.

intros [yli xri].
exists (inrT (GMult_prodT xLI yRI) (GMult_prodT xRI yLI) (GMult_pairT xri yli)).
change (Gidentical (GPlus (GPlus (GMult (yLf yli) x) (GMultAux y (xRf xri))) (AntiGame (GMult (yLf yli) (xRf xri))))
                   (GPlus (GPlus (GMult (xRf xri) y) (GMultAux x (yLf yli))) (AntiGame (GMult (xRf xri) (yLf yli))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (yLIH yli).
rewrite -> (xRIH xri).
rewrite -> (GPlusCommutative (GMult y (xRf xri))).
rewrite -> (xRIH xri (yLf yli)).
reflexivity.

intros [yri xli].
exists (inlT (GMult_prodT xLI yRI) (GMult_prodT xRI yLI) (GMult_pairT xli yri)).
change (Gidentical (GPlus (GPlus (GMult (yRf yri) x) (GMultAux y (xLf xli))) (AntiGame (GMult (yRf yri) (xLf xli))))
                   (GPlus (GPlus (GMult (xLf xli) y) (GMultAux x (yRf yri))) (AntiGame (GMult (xLf xli) (yRf yri))))).
rewrite <- GMultxGMultAux.
rewrite <- GMultxGMultAux.
rewrite -> (yRIH yri).
rewrite -> (xLIH xli).
rewrite -> (GPlusCommutative (GMult y (xLf xli))).
rewrite -> (xLIH xli (yRf yri)).
reflexivity.
Qed.

Theorem GlteGMultZeroxZero : forall x : Game, Glte (GMult Zero x) Zero.
Proof.
intros.
rewrite -> GMultCommutative.
apply GlteGMultxZeroZero.
Qed.

Theorem GlteZeroGMultZerox : forall x : Game, Glte Zero (GMult Zero x).
Proof.
intros.
rewrite -> GMultCommutative.
apply GlteZeroGMultxZero.
Qed.

Lemma GidZeroAntiZero : Gidentical Zero (AntiGame Zero).
Proof.
exists; intro; contradiction.
Qed.

Lemma GlteZeroAntiZero : Glte Zero (AntiGame Zero).
Proof.
rewrite <- GidZeroAntiZero.
reflexivity.
Qed.

Lemma GlteAntiZeroZero : Glte (AntiGame Zero) Zero.
Proof.
rewrite <- GidZeroAntiZero.
reflexivity.
Qed.

Lemma GlteGMultGMultAux : forall x y : Game, Glte (GMult x y) (GMultAux x y).
Proof.
intros x y.
rewrite <- (GMultxGMultAux x).
reflexivity.
Qed.

Lemma GlteGMultAuxGMult : forall x y : Game, Glte (GMultAux x y) (GMult x y).
Proof.
intros x y.
rewrite <- (GMultxGMultAux x).
reflexivity.
Qed.

Theorem GidxGMultxOne : forall x : Game, Gidentical x (GMult x One).
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in * .
assert
  (Mx1devel:
    (Gidentical (GMult x One)
      (Game_cons (GMult_prodT (GLeftIndex x) OnePointIndex) (GMult_prodT (GRightIndex x) (OnePointIndex))
	(fun lli : GMult_prodT (GLeftIndex x) (OnePointIndex) =>
	  let (xli, Oneli) := lli in
	  let xl := GLeftFun x xli in
	  let Onel := GLeftFun One Oneli in
            GPlus (GPlus (GMult xl One) (GMult x Zero)) (AntiGame (GMult xl Zero)))
	(fun rli : GMult_prodT (GRightIndex x) (OnePointIndex) =>
	  let (xri, Oneli) := rli in
	  let xr := GRightFun x xri in
	  let Onel := GLeftFun One Oneli in
	    GPlus (GPlus (GMult xr One) (GMult x Zero)) (AntiGame (GMult xr Zero)))))).
exists.

intros Mx1li; simpl in Mx1li; case Mx1li; clear Mx1li.
intros p; exists p.
reflexivity.
intro p; case p; clear p; contradiction.

intros Mx1ri; simpl in Mx1ri; case Mx1ri; clear Mx1ri.
intro p; case p; clear p; contradiction.
intros p; exists p.
reflexivity.

intros Mx1li; simpl in Mx1li.
exists (inlT _ (GMult_prodT xRI False) Mx1li).
reflexivity.

intros Mx1ri; simpl in Mx1ri.
exists (inrT (GMult_prodT xLI False) _ Mx1ri).
reflexivity.

rewrite Mx1devel.
clear Mx1devel.
exists.

intros.
exists (GMult_pairT xli OnePoint).
set (xl:=(GLeftFun x xli)) in * .
change (Gidentical xl (GPlus (GPlus (GMult xl One) (GMult x Zero)) (AntiGame (GMult xl Zero)))).
rewrite -> (GidGMultxZeroZero x).
rewrite <- (xLIH xli).
rewrite <- (GidxGPlusxZero xl).
rewrite -> (GidGMultxZeroZero xl).
rewrite <- (GidZeroAntiZero).
rewrite <- (GidxGPlusxZero xl).
reflexivity.

intros.
exists (GMult_pairT xri OnePoint).
set (xr:=(GRightFun x xri)) in * .
change (Gidentical xr (GPlus (GPlus (GMult xr One) (GMult x Zero)) (AntiGame (GMult xr Zero)))).
rewrite -> (GidGMultxZeroZero x).
rewrite <- (xRIH xri).
rewrite <- (GidxGPlusxZero xr).
rewrite -> (GidGMultxZeroZero xr).
rewrite <- (GidZeroAntiZero).
rewrite <- (GidxGPlusxZero xr).
reflexivity.


(* This case has alredy been proved, modulo symmetry of Gid *)
intros p; simpl in p; case p; clear p.
intros xli o; case o; clear o.
exists xli.
set (xl:=(GLeftFun x xli)) in * .
change (Gidentical (GPlus (GPlus (GMult xl One) (GMult x Zero)) (AntiGame (GMult xl Zero))) xl).
rewrite -> (GidGMultxZeroZero x).
rewrite <- (xLIH xli).
rewrite <- (GidxGPlusxZero xl).
rewrite -> (GidGMultxZeroZero xl).
rewrite <- (GidZeroAntiZero).
rewrite <- (GidxGPlusxZero xl).
reflexivity.

intros p; simpl in p; case p; clear p.
intros xri o; case o; clear o.
exists xri.
set (xr:=(GRightFun x xri)) in * .
change (Gidentical (GPlus (GPlus (GMult xr One) (GMult x Zero)) (AntiGame (GMult xr Zero))) xr).
rewrite -> (GidGMultxZeroZero x).
rewrite <- (xRIH xri).
rewrite <- (GidxGPlusxZero xr).
rewrite -> (GidGMultxZeroZero xr).
rewrite <- (GidZeroAntiZero).
rewrite <- (GidxGPlusxZero xr).
reflexivity.
Qed.

Lemma GidxGMultOnex : forall x : Game, Gidentical x (GMult One x).
Proof.
intros x.
rewrite GMultCommutative.
apply GidxGMultxOne.
Qed.

Theorem GltexGMultOnex : forall x : Game, Glte x (GMult One x).
Proof.
intros x.
rewrite <- (GidxGMultOnex x).
reflexivity.
Qed.

Theorem GlteGMultOnexx : forall x : Game, Glte (GMult One x) x.
Proof.
intros x.
rewrite <- (GidxGMultOnex x).
reflexivity.
Qed.

Theorem GMultCommutative_Geq : forall x y : Game, Geq (GMult x y) (GMult y x).
Proof.
intros.
rewrite <- (GMultCommutative x y).
reflexivity.
Qed.

Theorem GidGMultAntixyAntiGMultxy :
 forall x y : Game, Gidentical (GMult (AntiGame x) y) (AntiGame (GMult x y)).
Proof.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
exists.


intros MAxyli; simpl in MAxyli; case MAxyli; clear MAxyli.

intros p.
exists (inrT (GMult_prodT xLI yRI) (GMult_prodT xRI yLI) p).
destruct p as [xri yli].
set (xr:=xRf xri) in * .
set (yl:=yLf yli) in * .
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xr) y) (GMult (AntiGame x) yl)) (AntiGame (GMult (AntiGame xr) yl)))
    (AntiGame (GPlus (GPlus (GMult xr y) (GMult x yl)) (AntiGame (GMult xr yl))))).
rewrite -> (xRIH xri y).
rewrite -> (yLIH yli).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xRIH xri yl).
reflexivity.

intros p.
exists (inlT (GMult_prodT xLI yRI) (GMult_prodT xRI yLI) p).
destruct p as [xli yri].
set (xl:=xLf xli) in * .
set (yr:=yRf yri) in * .
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xl) y) (GMult (AntiGame x) yr)) (AntiGame (GMult (AntiGame xl) yr)))
    (AntiGame (GPlus (GPlus (GMult xl y) (GMult x yr)) (AntiGame (GMult xl yr))))).
rewrite -> (xLIH xli y).
rewrite -> (yRIH yri).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xLIH xli yr).
reflexivity.


intros MAxyri; simpl in MAxyri; case MAxyri; clear MAxyri.

intros p.
exists (inrT (GMult_prodT xLI yLI) (GMult_prodT xRI yRI) p).
destruct p as [xri yri].
set (xr:=xRf xri) in * .
set (yr:=yRf yri) in * .
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xr) y) (GMult (AntiGame x) yr)) (AntiGame (GMult (AntiGame xr) yr)))
    (AntiGame (GPlus (GPlus (GMult xr y) (GMult x yr)) (AntiGame (GMult xr yr))))).
rewrite -> (xRIH xri y).
rewrite -> (yRIH yri).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xRIH xri yr).
reflexivity.

intros p.
exists (inlT (GMult_prodT xLI yLI) (GMult_prodT xRI yRI) p).
destruct p as [xli yli].
set (xl:=xLf xli) in * .
set (yl:=yLf yli) in * .
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xl) y) (GMult (AntiGame x) yl)) (AntiGame (GMult (AntiGame xl) yl)))
    (AntiGame (GPlus (GPlus (GMult xl y) (GMult x yl)) (AntiGame (GMult xl yl))))).
rewrite -> (xLIH xli y).
rewrite -> (yLIH yli).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xLIH xli yl).
reflexivity.



(*The remaining cases are the previous ones with
  \forall and \exists swapped and modulo commutativity
  and subcases swapped *)
intros AMxyli; simpl in AMxyli; case AMxyli; clear AMxyli.

intros p.
exists (inrT (GMult_prodT xRI yLI) (GMult_prodT xLI yRI) p).
destruct p as [xli yri].
set (xl:=xLf xli) in * .
set (yr:=yRf yri) in * .
apply Gidentical_commutative.
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xl) y) (GMult (AntiGame x) yr)) (AntiGame (GMult (AntiGame xl) yr)))
    (AntiGame (GPlus (GPlus (GMult xl y) (GMult x yr)) (AntiGame (GMult xl yr))))).
rewrite -> (xLIH xli y).
rewrite -> (yRIH yri).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xLIH xli yr).
reflexivity.

intros p.
exists (inlT (GMult_prodT xRI yLI) (GMult_prodT xLI yRI) p).
destruct p as [xri yli].
set (xr:=xRf xri) in * .
set (yl:=yLf yli) in * .
apply Gidentical_commutative.
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xr) y) (GMult (AntiGame x) yl)) (AntiGame (GMult (AntiGame xr) yl)))
    (AntiGame (GPlus (GPlus (GMult xr y) (GMult x yl)) (AntiGame (GMult xr yl))))).
rewrite -> (xRIH xri y).
rewrite -> (yLIH yli).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xRIH xri yl).
reflexivity.


intros AMxyri; simpl in AMxyri; case AMxyri; clear AMxyri.

intros p.
exists (inrT (GMult_prodT xRI yRI) (GMult_prodT xLI yLI)  p).
destruct p as [xli yli].
set (xl:=xLf xli) in * .
set (yl:=yLf yli) in * .
apply Gidentical_commutative.
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xl) y) (GMult (AntiGame x) yl)) (AntiGame (GMult (AntiGame xl) yl)))
    (AntiGame (GPlus (GPlus (GMult xl y) (GMult x yl)) (AntiGame (GMult xl yl))))).
rewrite -> (xLIH xli y).
rewrite -> (yLIH yli).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xLIH xli yl).
reflexivity.

intros p.
exists (inlT (GMult_prodT xRI yRI) (GMult_prodT xLI yLI) p).
destruct p as [xri yri].
set (xr:=xRf xri) in * .
set (yr:=yRf yri) in * .
apply Gidentical_commutative.
change
  (Gidentical
    (GPlus (GPlus (GMult (AntiGame xr) y) (GMult (AntiGame x) yr)) (AntiGame (GMult (AntiGame xr) yr)))
    (AntiGame (GPlus (GPlus (GMult xr y) (GMult x yr)) (AntiGame (GMult xr yr))))).
rewrite -> (xRIH xri y).
rewrite -> (yRIH yri).
rewrite <- AntiGPlus.
rewrite <- AntiGPlus.
rewrite -> (xRIH xri yr).
reflexivity.
Qed.

Theorem GeqGMultAntixyAntiGMultxy :
 forall x y : Game, Geq (GMult (AntiGame x) y) (AntiGame (GMult x y)).
intros.
rewrite <- (GidGMultAntixyAntiGMultxy x y).
reflexivity.
Qed.

Theorem GidGMultxAntiyAntiGMultxy :
 forall x y : Game, Gidentical (GMult x (AntiGame y)) (AntiGame (GMult x y)).
Proof.
intros.
rewrite -> (GMultCommutative).
rewrite -> (GidGMultAntixyAntiGMultxy y x).
apply GAnti_MorphId.
apply GMultCommutative.
Qed.

Theorem GeqGMultxAntiyAntiGMultxy :
 forall x y : Game, Geq (GMult x (AntiGame y)) (AntiGame (GMult x y)).
Proof.
intros x y.
rewrite <- (GidGMultxAntiyAntiGMultxy x y).
reflexivity.
Qed.

Lemma Gltexlx: forall x:Game, forall xli:(GLeftIndex x), IsNumber x -> (Glte (GLeftFun x xli) x).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros xli Numx.
exists.

intros xlli.
right.
exists xli.
apply xLIH.
inversion Numx as [x' Numxl Numxr NGgtexlxr x'x]; clear x' x'x.
apply Numxl.

intros xri.
inversion Numx as [x' Numxl Numxr NGgtexlxr x'x]; clear x' x'x.
apply NGgtexlxr.
Qed.

Lemma Gltexxr: forall x:Game, forall xri:(GRightIndex x), IsNumber x -> (Glte x (GRightFun x xri)).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros xri Numx.
exists.

intros xli.
inversion Numx as [x' Numxl Numxr NGgtexlxr x'x]; clear x' x'x.
apply NGgtexlxr.

intros xrri.
left.
exists xri.
apply xRIH.
inversion Numx as [x' Numxl Numxr NGgtexlxr x'x]; clear x' x'x.
apply Numxr.
Qed.

Ltac cut_case t :=
  cut (t = t);
  [ pattern t at -1; case t | reflexivity ].

Ltac expl_case t :=
  cut_case t; intros until 1.

Lemma Number_GPlus_closed :
 forall x y : Game, IsNumber x -> IsNumber y -> IsNumber (GPlus x y).
Proof.
intros x.
induction x as [xLI xRI xLf xLIH xRf xRIH].
set (x := Game_cons xLI xRI xLf xRf) in |- * .
intros y.
induction y as [yLI yRI yLf yLIH yRf yRIH].
set (y := Game_cons yLI yRI yLf yRf) in |- * .
intros Numx Numy.
inversion Numx as [x' Numxl Numxr NGgtexlxr x'x]; clear x' x'x.
inversion Numy as [y' Numyl Numyr NGgteylyr y'y]; clear y' y'y.
exists.

intros Pxyli.
simpl in Pxyli.
destruct Pxyli as [xli | yli].
simpl; fold x y.
apply xLIH; try assumption.
apply Numxl.
simpl.
rewrite <- (GPlusxGPlusAux x).
apply yLIH; try assumption.
apply Numyl.

intros Pxyri.
simpl in Pxyri.
destruct Pxyri as [xri | yri].
simpl; fold x y.
apply xRIH; try assumption.
apply Numxr.
simpl.
rewrite <- (GPlusxGPlusAux x).
apply yRIH; try assumption.
apply Numyr.


intros Pxyli Pxyri.
simpl in Pxyli; simpl in Pxyri.
destruct Pxyli as [xli | yli]; destruct Pxyri as [xri | yri]; simpl; do 2 try rewrite <- (GPlusxGPlusAux x); fold x y.

apply GPlusNGgteLeft.
apply NGgtexlxr.
3: apply GPlusNGgteRight.
3: apply NGgteylyr.

right.
expl_case (yRf yri).
exists (inlT xLI LI xli).
simpl.
rewrite <- H.
apply GPlusGlteRight.
apply (Gltexxr y).
assumption.

left.
expl_case (yLf yli).
exists (inlT xRI RI xri).
simpl.
rewrite <- H.
apply GPlusGlteRight.
apply (Gltexlx y).
assumption.
Qed.

Theorem GMultDistrib :
 forall x y z : Game,
 Geq (GMult (GPlus x y) z) (GPlus (GMult x z) (GMult y z)).
Proof.
intros x.
induction x.
rename RI into xRI; rename LI into xLI; rename g into xLf; rename H into xLIH;
 rename g0 into xRf; rename H0 into xRIH.
set (x := Game_cons xLI xRI xLf xRf) in * .
intros y.
induction y.
rename RI into yRI; rename LI into yLI; rename g into yLf; rename H into yLIH;
 rename g0 into yRf; rename H0 into yRIH.
set (y := Game_cons yLI yRI yLf yRf) in * .
intros z.
induction z.
rename RI into zRI; rename LI into zLI; rename g into zLf; rename H into zLIH;
 rename g0 into zRf; rename H0 into zRIH.
set (z := Game_cons zLI zRI zLf zRf) in * .

split; exists.



intros MPxyzli; simpl in MPxyzli; destruct MPxyzli as [ [ [ xli | yli ] zli ] | [ [ xri | yri ] zri ]].

change
  (NGgte (GPlus (GPlus (GMult (GPlus (xLf xli) y) z) (GMult (GPlus x y) (zLf zli)))
                (AntiGame (GMult (GPlus (xLf xli) y) (zLf zli))))
         (GPlus (GMult x z) (GMult y z))).
right.
exists (inlT (sumT (GMult_prodT xLI zLI) (GMult_prodT xRI zRI))
             (sumT (GMult_prodT yLI zLI) (GMult_prodT yRI zRI))
	     (inlT (GMult_prodT xLI zLI) (GMult_prodT xRI zRI) (GMult_pairT xli zli))).
change
  (Glte (GPlus (GPlus (GMult (GPlus (xLf xli) y) z) (GMult (GPlus x y) (zLf zli)))
               (AntiGame (GMult (GPlus (xLf xli) y) (zLf zli))))
        (GPlus (GPlus (GPlus (GMult (xLf xli) z) (GMult x (zLf zli))) (AntiGame (GMult (xLf xli) (zLf zli))))
               (GMult y z))).
rewrite -> xLIH.
rewrite -> xLIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (GMult y (zLf zli)) (GPlus (AntiGame (GMult (xLf xli) (zLf zli)))
                    (AntiGame (GMult y (zLf zli))))).
rewrite <- GPlusAssociative.
rewrite -> (AntixPlusxZero).
rewrite <- (GidxGPlusxZero).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.

change
  (NGgte (GPlus (GPlus (GMult (GPlus x (yLf yli)) z) (GMult (GPlus x y) (zLf zli)))
                (AntiGame (GMult (GPlus x (yLf yli)) (zLf zli))))
         (GPlus (GMult x z) (GMult y z))).
right.
exists (inrT (sumT (GMult_prodT xLI zLI) (GMult_prodT xRI zRI))
             (sumT (GMult_prodT yLI zLI) (GMult_prodT yRI zRI))
	     (inlT (GMult_prodT yLI zLI) (GMult_prodT yRI zRI) (GMult_pairT yli zli))).
change
  (Glte (GPlus (GPlus (GMult (GPlus x (yLf yli)) z) (GMult (GPlus x y) (zLf zli)))
               (AntiGame (GMult (GPlus x (yLf yli)) (zLf zli))))
        (GPlus (GMult x z)
               (GPlus (GPlus (GMult (yLf yli) z) (GMult y (zLf zli))) (AntiGame (GMult (yLf yli) (zLf zli)))))).
rewrite -> yLIH.
rewrite -> yLIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zLf zli))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zLf zli))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
apply GPlusGlteRight.
rewrite GPlusCommutative.
reflexivity.

change
  (NGgte (GPlus (GPlus (GMult (GPlus (xRf xri) y) z) (GMult (GPlus x y) (zRf zri)))
                (AntiGame (GMult (GPlus (xRf xri) y) (zRf zri))))
         (GPlus (GMult x z) (GMult y z))).
right.
exists (inlT (sumT (GMult_prodT xLI zLI) (GMult_prodT xRI zRI))
             (sumT (GMult_prodT yLI zLI) (GMult_prodT yRI zRI))
	     (inrT (GMult_prodT xLI zLI) (GMult_prodT xRI zRI) (GMult_pairT xri zri))).
change
  (Glte (GPlus (GPlus (GMult (GPlus (xRf xri) y) z) (GMult (GPlus x y) (zRf zri)))
               (AntiGame (GMult (GPlus (xRf xri) y) (zRf zri))))
        (GPlus (GPlus (GPlus (GMult (xRf xri) z) (GMult x (zRf zri))) (AntiGame (GMult (xRf xri) (zRf zri))))
               (GMult y z))).
rewrite -> xRIH.
rewrite -> xRIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (GMult y (zRf zri)) (GPlus (AntiGame (GMult (xRf xri) (zRf zri)))
                    (AntiGame (GMult y (zRf zri))))).
rewrite <- GPlusAssociative.
rewrite -> (AntixPlusxZero).
rewrite <- (GidxGPlusxZero).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.

change
  (NGgte (GPlus (GPlus (GMult (GPlus x (yRf yri)) z) (GMult (GPlus x y) (zRf zri)))
                (AntiGame (GMult (GPlus x (yRf yri)) (zRf zri))))
         (GPlus (GMult x z) (GMult y z))).
right.
exists (inrT (sumT (GMult_prodT xLI zLI) (GMult_prodT xRI zRI))
             (sumT (GMult_prodT yLI zLI) (GMult_prodT yRI zRI))
	     (inrT (GMult_prodT yLI zLI) (GMult_prodT yRI zRI) (GMult_pairT yri zri))).
change
  (Glte (GPlus (GPlus (GMult (GPlus x (yRf yri)) z) (GMult (GPlus x y) (zRf zri)))
               (AntiGame (GMult (GPlus x (yRf yri)) (zRf zri))))
        (GPlus (GMult x z)
               (GPlus (GPlus (GMult (yRf yri) z) (GMult y (zRf zri))) (AntiGame (GMult (yRf yri) (zRf zri)))))).
rewrite -> yRIH.
rewrite -> yRIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zRf zri))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zRf zri))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
apply GPlusGlteRight.
rewrite GPlusCommutative.
reflexivity.


intros PMxyMyzri; simpl in PMxyMyzri; destruct PMxyMyzri as [ [ [ xli zri ] | [ xri zli ] ] | [ [ yli zri ] | [ yri zli ] ] ].

change
  (NGgte (GMult (GPlus x y) z)
         (GPlus (GPlus (GPlus (GMult (xLf xli) z) (GMult x (zRf zri))) (AntiGame (GMult (xLf xli) (zRf zri))))
	        (GMult y z))).
left.
exists (inlT (GMult_prodT (sumT xLI yLI) zRI)
             (GMult_prodT (sumT xRI yRI) zLI)
	     (GMult_pairT (inlT xLI yLI xli) zri)).
change
  (Glte (GPlus (GPlus (GMult (GPlus (xLf xli) y) z) (GMult (GPlus x y) (zRf zri))) (AntiGame (GMult (GPlus (xLf xli) y) (zRf zri))))
        (GPlus (GPlus (GPlus (GMult (xLf xli) z) (GMult x (zRf zri))) (AntiGame (GMult (xLf xli) (zRf zri))))
               (GMult y z))).
rewrite -> xLIH.
rewrite -> xLIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (AntiGame (GMult (xLf xli) (zRf zri))) (AntiGame (GMult y (zRf zri)))).
rewrite -> (GPlusAssociative (GMult y (zRf zri))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.

change
  (NGgte (GMult (GPlus x y) z)
         (GPlus (GPlus (GPlus (GMult (xRf xri) z) (GMult x (zLf zli))) (AntiGame (GMult (xRf xri) (zLf zli))))
	        (GMult y z))).
left.
exists (inrT (GMult_prodT (sumT xLI yLI) zRI)
             (GMult_prodT (sumT xRI yRI) zLI)
	     (GMult_pairT (inlT xRI yRI xri) zli)).
change
  (Glte (GPlus (GPlus (GMult (GPlus (xRf xri) y) z) (GMult (GPlus x y) (zLf zli))) (AntiGame (GMult (GPlus (xRf xri) y) (zLf zli))))
        (GPlus (GPlus (GPlus (GMult (xRf xri) z) (GMult x (zLf zli))) (AntiGame (GMult (xRf xri) (zLf zli))))
               (GMult y z))).
rewrite -> xRIH.
rewrite -> xRIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (AntiGame (GMult (xRf xri) (zLf zli))) (AntiGame (GMult y (zLf zli)))).
rewrite -> (GPlusAssociative (GMult y (zLf zli))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.


change
  (NGgte (GMult (GPlus x y) z)
         (GPlus (GMult x z)
	        (GPlus (GPlus (GMult (yLf yli) z) (GMult y (zRf zri))) (AntiGame (GMult (yLf yli) (zRf zri)))))).
left.
exists (inlT (GMult_prodT (sumT xLI yLI) zRI)
             (GMult_prodT (sumT xRI yRI) zLI)
	     (GMult_pairT (inrT xLI yLI yli) zri)).
change
  (Glte (GPlus (GPlus (GMult (GPlus x (yLf yli)) z) (GMult (GPlus x y) (zRf zri))) (AntiGame (GMult (GPlus x (yLf yli)) (zRf zri))))
        (GPlus (GMult x z)
	       (GPlus (GPlus (GMult (yLf yli) z) (GMult y (zRf zri))) (AntiGame (GMult (yLf yli) (zRf zri)))))).
rewrite -> yLIH.
rewrite -> yLIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zRf zri))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zRf zri))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
apply GPlusGlteRight.
rewrite GPlusCommutative.
reflexivity.

change
  (NGgte (GMult (GPlus x y) z)
         (GPlus (GMult x z) (GPlus (GPlus (GMult (yRf yri) z) (GMult y (zLf zli))) (AntiGame (GMult (yRf yri) (zLf zli)))))).
left.
exists (inrT (GMult_prodT (sumT xLI yLI) zRI)
             (GMult_prodT (sumT xRI yRI) zLI)
             (GMult_pairT (inrT xRI yRI yri) zli)).
change
  (Glte (GPlus (GPlus (GMult (GPlus x (yRf yri)) z) (GMult (GPlus x y) (zLf zli))) (AntiGame (GMult (GPlus x (yRf yri)) (zLf zli))))
        (GPlus (GMult x z) (GPlus (GPlus (GMult (yRf yri) z) (GMult y (zLf zli))) (AntiGame (GMult (yRf yri) (zLf zli)))))).
rewrite -> yRIH.
rewrite -> yRIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zLf zli))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zLf zli))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
apply GPlusGlteRight.
rewrite GPlusCommutative.
reflexivity.



intros PMxyMyzli; simpl in PMxyMyzli; destruct PMxyMyzli as [ [ [ xli zli ] | [ xri zri ] ] | [ [ yli zli ] | [ yri zri ] ] ].

change
  (NGgte (GPlus (GPlus (GPlus (GMult (xLf xli) z) (GMult x (zLf zli))) (AntiGame (GMult (xLf xli) (zLf zli))))
	        (GMult y z))
         (GMult (GPlus x y) z)).
right.
exists (inlT (GMult_prodT (sumT xLI yLI) zLI)
             (GMult_prodT (sumT xRI yRI) zRI)
	     (GMult_pairT (inlT xLI yLI xli) zli)).
change
  (Glte (GPlus (GPlus (GPlus (GMult (xLf xli) z) (GMult x (zLf zli))) (AntiGame (GMult (xLf xli) (zLf zli))))
               (GMult y z))
        (GPlus (GPlus (GMult (GPlus (xLf xli) y) z) (GMult (GPlus x y) (zLf zli))) (AntiGame (GMult (GPlus (xLf xli) y) (zLf zli))))).
rewrite -> xLIH.
rewrite -> xLIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (AntiGame (GMult (xLf xli) (zLf zli))) (AntiGame (GMult y (zLf zli)))).
rewrite -> (GPlusAssociative (GMult y (zLf zli))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.

change
  (NGgte (GPlus (GPlus (GPlus (GMult (xRf xri) z) (GMult x (zRf zri))) (AntiGame (GMult (xRf xri) (zRf zri))))
	        (GMult y z))
         (GMult (GPlus x y) z)).
right.
exists (inrT (GMult_prodT (sumT xLI yLI) zLI)
             (GMult_prodT (sumT xRI yRI) zRI)
	     (GMult_pairT (inlT xRI yRI xri) zri)).
change
  (Glte (GPlus (GPlus (GPlus (GMult (xRf xri) z) (GMult x (zRf zri))) (AntiGame (GMult (xRf xri) (zRf zri))))
               (GMult y z))
        (GPlus (GPlus (GMult (GPlus (xRf xri) y) z) (GMult (GPlus x y) (zRf zri))) (AntiGame (GMult (GPlus (xRf xri) y) (zRf zri))))).
rewrite -> xRIH.
rewrite -> xRIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (AntiGame (GMult (xRf xri) (zRf zri))) (AntiGame (GMult y (zRf zri)))).
rewrite -> (GPlusAssociative (GMult y (zRf zri))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.


change
  (NGgte (GPlus (GMult x z)
	        (GPlus (GPlus (GMult (yLf yli) z) (GMult y (zLf zli))) (AntiGame (GMult (yLf yli) (zLf zli)))))(GMult (GPlus x y) z)).
right.
exists (inlT (GMult_prodT (sumT xLI yLI) zLI)
             (GMult_prodT (sumT xRI yRI) zRI)
	     (GMult_pairT (inrT xLI yLI yli) zli)).
change
  (Glte (GPlus (GMult x z)
	       (GPlus (GPlus (GMult (yLf yli) z) (GMult y (zLf zli))) (AntiGame (GMult (yLf yli) (zLf zli)))))
        (GPlus (GPlus (GMult (GPlus x (yLf yli)) z) (GMult (GPlus x y) (zLf zli))) (AntiGame (GMult (GPlus x (yLf yli)) (zLf zli))))).
rewrite -> yLIH.
rewrite -> yLIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zLf zli))).
rewrite -> (GPlusCommutative (GMult y (zLf zli))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zLf zli))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
reflexivity.

change
  (NGgte (GPlus (GMult x z) (GPlus (GPlus (GMult (yRf yri) z) (GMult y (zRf zri))) (AntiGame (GMult (yRf yri) (zRf zri)))))
         (GMult (GPlus x y) z)).
right.
exists (inrT (GMult_prodT (sumT xLI yLI) zLI)
             (GMult_prodT (sumT xRI yRI) zRI)
             (GMult_pairT (inrT xRI yRI yri) zri)).
change
  (Glte (GPlus (GMult x z) (GPlus (GPlus (GMult (yRf yri) z) (GMult y (zRf zri))) (AntiGame (GMult (yRf yri) (zRf zri)))))
        (GPlus (GPlus (GMult (GPlus x (yRf yri)) z) (GMult (GPlus x y) (zRf zri))) (AntiGame (GMult (GPlus x (yRf yri)) (zRf zri))))).
rewrite -> yRIH.
rewrite -> yRIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zRf zri))).
rewrite -> (GPlusCommutative (GMult y (zRf zri))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zRf zri))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
reflexivity.


intros MPxyzri; simpl in MPxyzri; destruct MPxyzri as [ [ [ xli | yli ] zri ] | [ [ xri | yri ] zli ]].

change
  (NGgte (GPlus (GMult x z) (GMult y z))
         (GPlus (GPlus (GMult (GPlus (xLf xli) y) z) (GMult (GPlus x y) (zRf zri)))
                (AntiGame (GMult (GPlus (xLf xli) y) (zRf zri))))).
left.
exists (inlT (sumT (GMult_prodT xLI zRI) (GMult_prodT xRI zLI))
             (sumT (GMult_prodT yLI zRI) (GMult_prodT yRI zLI))
	     (inlT (GMult_prodT xLI zRI) (GMult_prodT xRI zLI) (GMult_pairT xli zri))).
change
  (Glte (GPlus (GPlus (GPlus (GMult (xLf xli) z) (GMult x (zRf zri))) (AntiGame (GMult (xLf xli) (zRf zri))))
               (GMult y z))
        (GPlus (GPlus (GMult (GPlus (xLf xli) y) z) (GMult (GPlus x y) (zRf zri)))
               (AntiGame (GMult (GPlus (xLf xli) y) (zRf zri))))).
rewrite -> xLIH.
rewrite -> xLIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (GMult y (zRf zri)) (GPlus (AntiGame (GMult (xLf xli) (zRf zri)))
                    (AntiGame (GMult y (zRf zri))))).
rewrite <- GPlusAssociative.
rewrite -> (AntixPlusxZero).
rewrite <- (GidxGPlusxZero).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.

change
  (NGgte (GPlus (GMult x z) (GMult y z))
         (GPlus (GPlus (GMult (GPlus x (yLf yli)) z) (GMult (GPlus x y) (zRf zri)))
                (AntiGame (GMult (GPlus x (yLf yli)) (zRf zri))))).
left.
exists (inrT (sumT (GMult_prodT xLI zRI) (GMult_prodT xRI zLI))
             (sumT (GMult_prodT yLI zRI) (GMult_prodT yRI zLI))
	     (inlT (GMult_prodT yLI zRI) (GMult_prodT yRI zLI) (GMult_pairT yli zri))).
change
  (Glte (GPlus (GMult x z)
               (GPlus (GPlus (GMult (yLf yli) z) (GMult y (zRf zri))) (AntiGame (GMult (yLf yli) (zRf zri)))))
        (GPlus (GPlus (GMult (GPlus x (yLf yli)) z) (GMult (GPlus x y) (zRf zri)))
               (AntiGame (GMult (GPlus x (yLf yli)) (zRf zri))))).
rewrite -> yLIH.
rewrite -> yLIH.
rewrite zRIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zRf zri))).
rewrite -> (GPlusCommutative (GMult y (zRf zri))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zRf zri))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
reflexivity.

change
  (NGgte (GPlus (GMult x z) (GMult y z))
         (GPlus (GPlus (GMult (GPlus (xRf xri) y) z) (GMult (GPlus x y) (zLf zli)))
                (AntiGame (GMult (GPlus (xRf xri) y) (zLf zli))))).
left.
exists (inlT (sumT (GMult_prodT xLI zRI) (GMult_prodT xRI zLI))
             (sumT (GMult_prodT yLI zRI) (GMult_prodT yRI zLI))
	     (inrT (GMult_prodT xLI zRI) (GMult_prodT xRI zLI) (GMult_pairT xri zli))).
change
  (Glte (GPlus (GPlus (GPlus (GMult (xRf xri) z) (GMult x (zLf zli))) (AntiGame (GMult (xRf xri) (zLf zli))))
               (GMult y z))
        (GPlus (GPlus (GMult (GPlus (xRf xri) y) z) (GMult (GPlus x y) (zLf zli)))
               (AntiGame (GMult (GPlus (xRf xri) y) (zLf zli))))).
rewrite -> xRIH.
rewrite -> xRIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite (GPlusCommutative (GMult y (zLf zli)) (GPlus (AntiGame (GMult (xRf xri) (zLf zli)))
                    (AntiGame (GMult y (zLf zli))))).
rewrite <- GPlusAssociative.
rewrite -> (AntixPlusxZero).
rewrite <- (GidxGPlusxZero).
apply GPlusGlteRight.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
rewrite GPlusCommutative.
rewrite <- GPlusAssociative.
reflexivity.

change
  (NGgte (GPlus (GMult x z) (GMult y z))
         (GPlus (GPlus (GMult (GPlus x (yRf yri)) z) (GMult (GPlus x y) (zLf zli)))
                (AntiGame (GMult (GPlus x (yRf yri)) (zLf zli))))).
left.
exists (inrT (sumT (GMult_prodT xLI zRI) (GMult_prodT xRI zLI))
             (sumT (GMult_prodT yLI zRI) (GMult_prodT yRI zLI))
	     (inrT (GMult_prodT yLI zRI) (GMult_prodT yRI zLI) (GMult_pairT yri zli))).
change
  (Glte (GPlus (GMult x z)
               (GPlus (GPlus (GMult (yRf yri) z) (GMult y (zLf zli))) (AntiGame (GMult (yRf yri) (zLf zli)))))
        (GPlus (GPlus (GMult (GPlus x (yRf yri)) z) (GMult (GPlus x y) (zLf zli)))
               (AntiGame (GMult (GPlus x (yRf yri)) (zLf zli))))).
rewrite -> yRIH.
rewrite -> yRIH.
rewrite zLIH.
rewrite AntiGPlus.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite <- GPlusAssociative.
rewrite -> (GPlusCommutative (GMult y (zLf zli))).
rewrite -> (GPlusCommutative (GMult y (zLf zli))).
rewrite <- GPlusAssociative.
rewrite -> (GPlusAssociative (GMult x (zLf zli))).
rewrite -> (xPlusAntixZero).
rewrite <- (GidxGPlusZerox).
reflexivity.
Qed.