proposition: Lemma processPackets_num_monotonic : forall n l n' l', processPackets n l = (n', l') -> n' >= n.
proof: Proof. Proof using. induction l; intros; simpl in *. - intros. find_inversion. intuition. - break_match. find_inversion. find_insterU. find_insterU. conclude_using eauto. lia. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)