proposition: Lemma fold_right_higher_is_higher {A} : forall (f : A -> nat) ns x, (forall r, List.In r ns -> f r <= x) -> fold_right (fun n acc => max (f n) acc) 0 ns <= x.
proof: Proof. induction ns; simpl; intros; [ apply le_0_n | ]. apply Nat.max_lub. apply H; left; auto. apply IHns; intros; apply H; right; auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts