proposition: Lemma list_helper: forall {T: Type} (l: list T) (f: T -> nat) (big: nat), lt (fold_right (fun e acc => max (f e) acc) 0 l) big -> ~ List.In big (map f l).
proof: Proof. induction l. - auto. - unfold not; intros f big Hbig H. cbn in Hbig. cbn in H. pose proof (Nat.max_spec (f a) (fold_right (fun (e : T) (acc : nat) => Init.Nat.max (f e) acc) 0 l)) as Hmax. destruct Hmax as [[Hlt Hmax] | [Hlt Hmax]]; rewrite Hmax in Hbig; destruct H as [H | H]. + subst big. pose proof (lt_trans _ _ _ Hlt Hbig). apply lt_irrefl in H. auto. + apply (IHl f big Hbig H). + subst big. apply lt_irrefl in Hbig. auto. + pose proof (le_lt_trans _ _ _ Hlt Hbig). apply (IHl f big H0 H). Qed.
imports: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields Coq.Sets.Ensembles