gistfile1.txt

Fixpoint fin_of_nat (m n : nat) : fin n + {p | m = n + p} :=
  match n with
    | 0 => inr (exist _ m eq_refl)  
    | S n' =>
      match m with
        | 0 => inl None
        | S m' =>
          match fin_of_nat m' n' with
            | inl f => inl (Some f) 
            | inr (exist _ x H) => inr (exist _ x (f_equal _ H))
          end
      end
  end.

Lemma fin_of_nat_fin_to_nat :
  forall (n : nat) (a : fin n),
    fin_of_nat (fin_to_nat a) n = inl a.
Proof.
  induction n; simpl; intuition.
  destruct a; simpl in *; auto.
  now rewrite IHn.
Qed.