proposition: Lemma Vmax_forall : forall n (v : nats n) p, Vmax v <= p -> Vforall (fun n => n <= p) v.
proof: Proof. intros n v p. elim v. intro. simpl. auto. simpl. intros h n' t Hrec H. split. eapply Nat.le_trans. apply (Nat.le_max_l h (Vmax t)). hyp. apply (Hrec (Nat.le_trans (Nat.le_max_r h (Vmax t)) H)). Qed.
imports: CoLoR(VecUtil NatUtil LogicUtil)