proposition: Theorem all_intervals_add : forall (l:list(nat*nat))(k p n:nat), n-p < k <= n -> all_intervals k l -> all_intervals k ((p,n)::l).
proof: Proof. intros l k p n Hint Hai l1; case l1. - intros l2 p' n' Heq; injection Heq; intros Hl Hn' Hp'; rewrite <- Hn'; rewrite <- Hp'; auto. - simpl; clear l1; intros fst_elem l1 l2 p' n' Heq; injection Heq; intros Hl Hfst; apply (Hai l1 l2); assumption. Qed.
imports: List Arith