proposition: Lemma processPackets_correct : forall n l n' l', processPackets n l = (n', l') -> forall p, In p l' -> n' > (tmNum (snd p)).
proof: Proof. Proof using. induction l; intros; simpl in *. - find_inversion. simpl in *. intuition. - break_match. find_inversion. simpl in *. intuition. + subst; simpl; lia. + apply (Nat.lt_le_trans _ n0). * apply (IHl _ l0); auto. * auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)