(* The trichotomy property of natural numbers. *)

Module trich Import lib_nat_Lt;

[i,j:nat];

Inductive [Trich : Type]
Constructors
[LT: (Lt i j)->Trich]
[GT: (Lt j i)->Trich]
[EQ: (Eq i j)->Trich];
Discharge i;

Goal {x:nat} Trich zero x;
intros;
Induction x;
Refine EQ;
Refine Eq_refl;
intros xx t;
Refine LT;
Refine zero_Lt_suc_n;
Save trichZero;

Goal {i,j|nat} (Trich i j) -> Trich j i;
intros i j T;
Induction T;
Refine GT;
Refine LT;
intros eq;
Refine EQ;
Refine Eq_sym;
Immed;
Save trich_sym;

Goal {i,j:nat} Trich i j;
intros i;
Refine nat_elim [i:nat] {j:nat} Trich i j;
intros j ;
Refine trichZero;
intros ii T j;
Refine nat_elim [j:nat] Trich (suc ii) j;
Refine GT ;
Refine zero_Lt_suc_n ;
intros jj _;
Induction T jj;
intros lt;
Refine LT;
Refine Lt_resp_suc;
Immed;
intros lt;
Refine GT;
Refine Lt_resp_suc;
Immed;
intros eq;
Refine EQ;
Refine Eq_resp suc;
Immed;
Save trich;

(* Simple elimination for Trich *)
Goal {i,j:nat}{P|Type} ((Lt i j)->P) -> ((Lt j i)->P) -> ((Eq i j)->P) -> P;
intros i j P A B C;
Refine Trich_elim i j ([_:Trich i j]P);
Immed;
Refine trich i j;
Save Trich_rec;

(* Trichotomy exclusions *)
[ not_Lt_Eq = Lt_not_Eq ];

Goal {i,j:nat} (Lt i j)->(Lt j i)->absurd;
intros i j lt gt ;
Refine not_refl_Lt i ;
Refine Lt_trans ;
Refine j ;
Immed ;
Save not_Lt_Gt ;

Goal {i,j:nat} (Lt j i)->(Eq i j)->absurd;
intros i j lt eq ;
Refine Lt_not_Eq j i ;
Immed ;
Refine Eq_sym ;
Immed ;
Save not_Gt_Eq ;