proposition: Lemma max_v_lub : forall n (v: t nat n) y, (Forall (fun x => x <= y) v) -> max_v v <= y.
proof: Proof. induction n. - intros v; rewrite (t_0_nil _ v); cbn. intros; auto with arith. - intros v; rewrite (decomp _ _ v); cbn. intros; destruct (Forall_inv _ _ _ _ H). apply Nat.max_lub; auto. Qed.