Library schutte.Minus

Add LoadPath "../prelude".
Add LoadPath "../hilbert".

Require Import Arith.
Require Import Epsilon.
Require Import Ensembles.
Require Import Schutte.
Require Import Ordering_Functions.
Require Import PartialFun.
Require Import Plus.
Set Implicit Arguments.

Definition minus (alpha beta :OT):= iota inh_OT
                   (fun gamma => ordinal gamma /\ beta + gamma = alpha).

Notation "alpha - beta" := (minus alpha beta):ord_scope.

Lemma minus_a_zero : forall alpha, ordinal alpha -> alpha - zero = alpha.
Proof.
 intros.
 pattern (alpha-zero).
 unfold minus.
 pattern (iota inh_OT (fun gamma : OT => ordinal gamma /\
                                         zero + gamma = alpha)).
 hilbert_e.
 exists alpha;split.
 rewrite zero_plus_alpha;auto.

 intros a' (Ha',e); rewrite zero_plus_alpha in e;auto.
 intros a (Oa,ea);rewrite zero_plus_alpha in ea;auto.
Qed.

Lemma minus_defined : forall alpha beta, alpha <= beta ->
    ex (unique (fun gamma => ordinal gamma /\ alpha + gamma = beta)).
Proof.
 intros alpha beta H.
 case (minus_exists H).
 intros diff (Hdiff,ediff).
 exists diff;repeat split;auto.
 intros diff' (odiff',ediff').
 subst beta.
 rewrite (plus_reg_r _ _ _ (le_ordinal H) odiff' Hdiff ediff');auto.
Qed.


Lemma minus_a_a : forall alpha, ordinal alpha ->
                                alpha - alpha = zero.
Proof.
 intros a Oa.
 pattern (a-a).
 hilbert_e.


 generalize (minus_defined (le_refl a Oa));auto with schutte.
 destruct 1 as (H1,H2).
 pattern a at 2 in H2; rewrite <- alpha_plus_zero in H2.
rewrite (plus_reg_r _ _ _ Oa H1 ordinal_zero H2);auto.
auto.
Qed.

Lemma minus_le : forall alpha beta, beta <= alpha ->
                                    alpha - beta <= alpha.
Proof.
 intros alpha beta H.
 pattern (alpha-beta);hilbert_e.
  generalize (minus_defined H);auto with schutte.
 intros a (Ha,Ha').
 subst alpha.
 apply le_plus_r;ordi.
Qed.

Lemma plus_minus :forall alpha beta, beta <= alpha ->
                                    alpha = beta + (alpha - beta).
Proof.
 intros alpha beta H.
 pattern (alpha-beta);hilbert_e.
  generalize (minus_defined H);auto with schutte.
  symmetry;tauto.
Qed.