proposition: Lemma Vmax_in : forall x n (v : nats n), Vin x v -> x <= Vmax v.
proof: Proof. induction v; simpl; intros. contr. destruct H. subst h. apply le_max_intro_l. apply Nat.le_refl. apply le_max_intro_r. auto. Qed.
imports: CoLoR(VecUtil NatUtil LogicUtil)