proposition: Lemma Nth_make : forall i n v, i < n -> Nth i (make n v) v.
proof: Proof. Proof using. Hint Constructors Nth. introv. gen n; induction i; introv E; destruct n; try solve [ false; math ]. { constructors. } { rewrite make_succ. applys Nth_succ. applys~ IHi. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)