proposition: Theorem all_greater_than_one_add : forall l n p, 1 < p -> all_greater_than_one l -> all_greater_than_one ((p,n)::l).
proof: Proof. intros l n p Hlt Hal l1; case l1. - simpl; intros l2 p' n' Heq; injection Heq; intros Hl2 Hn' Hp'; rewrite <- Hp'; assumption. - clear l1; simpl; intros fst_elem l1 l2 p' n' Heq; injection Heq; intros Hl Hfst; apply (Hal l1 l2 p' n'); assumption. Qed.
imports: List Arith