proposition: Lemma proj_le_max : forall n, forall v : t nat n, forall k (H: k < n), v_apply (evalProjFunc n k H) v <= max_v v.
proof: Proof. induction n. - cbn; intros; lia. - intros; specialize (IHn (tl v)); cbn. destruct (Nat.eq_dec k n). + cbn; rewrite (decomp _ _ v); cbn; rewrite evalList_Const; apply Nat.le_max_l. + assert (H0: k <= n) by lia; rewrite Nat.lt_eq_cases in H0. destruct H0. * replace v with (cons (hd v) (tl v)) at 1; cbn. -- transitivity (max_v (tl v)); auto. apply max_v_tl. -- symmetry; apply decomp. * now destruct n0. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)