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.