proposition: Lemma max_v_ge : forall n (v: t nat n) y, In y v -> y <= max_v v.
proof: Proof. induction n. - intros v; rewrite (t_0_nil _ v); cbn; inversion 1. - intros v; rewrite (decomp _ _ v); cbn; intros; destruct (In_cases _ _ H). + cbn in H0; subst; apply Nat.le_max_l. + cbn in H0; specialize (IHn _ _ H0); lia. Qed.