proposition: Theorem all_first_less_than_S : forall k l, all_first_less_than k l -> all_first_less_than (S k) l.
proof: Proof. intros k l; elim l. - intros Haf l1 l2 p n Heq; elim (absurd_decompose_list _ _ _ _ Heq). - intros (p,n) l0 Hrec Haf l1. case l1. + intros l2 p' n' Heq; generalize (Haf nil l2 p' n' Heq); intros Hpltk. auto with arith. + simpl; clear l1; intros fst_elem l1 l2 p' n' Heq. injection Heq; intros; apply (Hrec (all_first_less_than_transmit _ _ _ Haf) l1 l2 p' n'); assumption. Qed.
imports: List Arith