proposition: Lemma make_pos : forall n v, n > 0 -> make n v = v::(make (n-1) v).
proof: Proof. Proof using. introv E. destruct n. { math. } { rewrite make_succ. fequals_rec. math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)