proposition: Lemma nth_in_or_default : forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}.
proof: Proof. intros n l d; revert n; induction l as [|? ? IHl]. - intro n; right; destruct n; trivial. - intros [|n]; simpl. * left; auto. * destruct (IHl n); auto. Qed.
imports: PeanoNat