finite_ordinal.v

Set Printing Coercions.
Require Import Omega.

Inductive hoge (n:nat) : Type :=
| fuga (m:nat) : m < n -> hoge n.

Coercion nat_of_hoge {n:nat} (h : hoge n) :=
  match h with
  | fuga _ n _ => n
  end.

Lemma _0_2 : 0 < 2. Proof. omega. Qed.
Lemma _1_2 : 1 < 2. Proof. omega. Qed.
Lemma _0_3 : 0 < 3. Proof. omega. Qed.
Lemma _1_3 : 1 < 3. Proof. omega. Qed.
Lemma _2_3 : 2 < 3. Proof. omega. Qed.

Check fuga 3 0 _0_3.
(* fuga 3 0 _0_3 *)
(*      : hoge 3 *)

Check fuga 3 1 _1_3.
(* fuga 3 1 _1_3 *)
(*      : hoge 3 *)

Check fuga 3 2 _2_3.
(* fuga 3 2 _2_3 *)
(*      : hoge 3 *)

Definition f2_1 := fuga 2 1 _1_2.
Definition f3_2 := fuga 3 2 _2_3.

Check f2_1 + f3_2.
(* nat_of_hoge f2_1 + nat_of_hoge f3_2 *)
(*      : nat                          *)
Eval compute in f2_1 + f3_2.
     (* = 3   *)
     (* : nat *)