proposition: Lemma In_L_aux : forall k (h : k<n) i (p : i<n), i <= k -> In (N_ p) (L_aux h).
proof: Proof. induction k; simpl; intros. left. apply N_eq; simpl. lia. destruct (eq_nat_dec (S k) i). left. apply N_eq; simpl. hyp. right. apply IHk. lia. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)