proposition: Lemma nth_default_gt_length : forall l d n, n >= length l -> nth_default d n l = d.
proof: Proof. Proof using. induction l as [|l']; introv N; rew_list in *. { auto. } { destruct n as [|n']. { false; math. } simpl. rewrite~ IHl. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)