proposition: Theorem all_first_less_than_transmit : forall k (p:nat*nat)(l: list(nat*nat)), all_first_less_than k (p::l) -> all_first_less_than k l.
proof: Proof. intros k; exact (all_list_transmit (fun p n => p < k)). Qed.
imports: List Arith