proposition: Lemma processPackets_ge_start : 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 *. - invcs H. intuition. - break_match. invcs H. intuition. + subst. simpl. apply processPackets_num_monotonic in Heqp0. intuition. + specialize (IHl n0 l0). apply IHl; auto. Qed.
imports: Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(SeqNum)