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