proposition: Lemma Vmax_app_cons : forall n1 (v1 : nats n1) p n2 (v2 : nats n2), p <= Vmax (Vapp v1 (Vcons p v2)).
proof: Proof. intros. elim v1. simpl. auto with arith. intros a n' w H. simpl. eapply Nat.le_trans. apply H. auto with arith. Qed.
imports: CoLoR(VecUtil NatUtil LogicUtil)