proposition: Lemma nth_make : forall i n v, i < n -> nth i (make n v) = v.
proof: Proof. Proof using. intros. applys nth_of_Nth. applys~ Nth_make. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)