proposition: Lemma map_N_val_L_aux n : forall k (hk : k<n), map N_val (L_aux hk) = nats_decr_lt (S k).
proof: Proof. induction k; intro hk; simpl. refl. rewrite IHk. refl. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)