From Coq Require Import Arith Logic.Epsilon Ensembles.
From ZornsLemma Require Import CountableTypes.
From hydras Require Export Schutte_basics Ordering_Functions
     PartialFun Countable MoreEpsilonIota.
Set Implicit Arguments.
From hydras Require Export STDPP_compat.

Definition plus alpha := ord (ge alpha).
Infix "+" := plus : schutte_scope.

Fixpoint mult_Sn (alpha:Ord)(n:nat){struct n} :Ord :=
 match n with 0 ⇒ alpha
            | S p ⇒ mult_Sn alpha p + alpha
 end.

Definition mult_fin_r alpha n :=
  match n with
      0 ⇒ zero
    | S p ⇒ mult_Sn alpha p
  end.

Infix "×" := mult_fin_r : schutte_scope.

Lemma Unbounded_ge (alpha : Ord) : Unbounded (ge alpha).

Lemma ge_o_segment (alpha : Ord) :
 the_ordering_segment (ge alpha) = ordinal.

Lemma plus_ordering (alpha : Ord) :
  ordering_function (plus alpha)
                    ordinal
                    (ge alpha).

Lemma plus_elim (alpha : Ord) :
  ∀ P : (Ord→Ord)->Prop,
    (∀ f: Ord→Ord,
        ordering_function f ordinal (ge alpha)→ P f) →
    P (plus alpha).

Lemma normal_plus_alpha (alpha : Ord) :
  normal (plus alpha) (ge alpha).

Lemma alpha_plus_zero (alpha: Ord): alpha + zero = alpha.
Remark ge_zero : (ge zero : Ensemble Ord) = ordinal.


Lemma zero_plus_alpha (alpha : Ord): zero + alpha = alpha.

Lemma le_plus_l (alpha beta : Ord) : alpha ≤ alpha + beta.
Lemma le_plus_r (alpha beta : Ord) : beta ≤ alpha + beta.
Lemma plus_mono_r (alpha beta gamma : Ord) :
  beta < gamma → alpha + beta < alpha + gamma.
Lemma plus_of_succ (alpha beta : Ord) :
  alpha + (succ beta) = succ (alpha + beta).

Lemma plus_mono_r_weak (alpha beta gamma : Ord) :
  beta ≤ gamma → alpha + beta ≤ alpha + gamma.

Lemma plus_reg_r (alpha beta gamma : Ord) :
  alpha + beta = alpha + gamma → beta = gamma.

Lemma succ_is_plus_1 alpha : succ alpha = alpha + 1.

Lemma alpha_plus_sup (alpha : Ord) (A : Ensemble Ord) :
    Inhabited A →
    Countable A →
    alpha + |_| A = |_| (image A (plus alpha)).

Lemma plus_limit (alpha beta : Ord)
  : is_limit beta →
    alpha + beta = |_| (image (members beta) (plus alpha)).

Lemma plus_FF : ∀ i j, F (i + j) = F i + F j.

Lemma one_plus_omega : 1 + omega = omega.

Lemma minus_exists (alpha beta : Ord) :
  alpha ≤ beta →
  ∃ gamma, alpha + gamma = beta.

Section proof_of_associativity.
  Variables alpha beta : Ord.

  Lemma plus_assoc1 (gamma : Ord) :
    alpha + beta ≤ alpha + (beta + gamma) .

  Lemma plus_assoc2 (gamma : Ord) :
    alpha + beta ≤ gamma →
    ∃ khi, gamma = alpha + (beta + khi).

  Let f_alpha_beta := plus (alpha + beta).

  Let g_alpha_beta gamma := alpha + (beta + gamma).

  Remark of_g : ordering_function g_alpha_beta ordinal (ge (alpha+beta)).

  Lemma of_u : fun_equiv f_alpha_beta g_alpha_beta ordinal ordinal.

  Lemma plus_assoc3 (gamma : Ord) :
    f_alpha_beta gamma = g_alpha_beta gamma.

  Lemma plus_assoc' (gamma : Ord) :
    alpha + (beta + gamma) = (alpha + beta) + gamma.

End proof_of_associativity.

#[global] Instance plus_assoc: Assoc eq plus.

Lemma one_plus_infinite (alpha : Ord) :
  omega ≤ alpha → 1 + alpha = alpha.


Lemma finite_plus_infinite (n : nat) (alpha : Ord) :
  omega ≤ alpha → n + alpha = alpha.
Example L_3_plus_omega : 3 + omega = omega.

Lemma plus_mono_weak_l : ∀ alpha beta gamma,
                          alpha ≤ beta → alpha + gamma ≤ beta + gamma.

Lemma plus_mono_bi : ∀ alpha beta gamma delta,
                        alpha ≤ gamma →
                        beta < delta →
                        alpha + beta < gamma + delta.

Lemma mult_fin_r_one : ∀ n, (F 1) × S n = F (S n).

Lemma mult_fin_r_mono : ∀ alpha beta , alpha < beta →
   ∀ n, alpha × S n < beta × S n.

Lemma le_a_mult_Sn_a : ∀ alpha n, ordinal alpha →
                                       alpha ≤ alpha × S n.

Lemma mult_Sn_mono2 : ∀ a, zero < a →
                         ∀ n p, (n < p)%nat → a × S n < a × S p.

Lemma mult_Sn_mono3 : ∀ alpha, zero < alpha →
                         ∀ n p, (n < p)%nat → alpha × S n + alpha
                                                    ≤ alpha × S p.