gistfile1.txt

Require Import Arith.

Fixpoint fin_of_nat (m n : nat) : fin n + {m >= n} :=
  match n with
    | 0 => inright (Nat.le_0_l _)
    | S n' =>
      match m with
        | 0 => inleft None
        | S m' =>
          match fin_of_nat m' n' with
            | inleft f => inleft (Some f)
            | inright pf => inright (gt_le_S _ _ (le_lt_n_Sm _ _ pf))
          end
      end
  end.