proposition: Lemma sec_binary_infinite_chain : forall (X:Type) R (f : nat -> X), almost_full R -> forall (k:nat), exists n, exists m, (n > m) /\ (m >= k) /\ R (f m) (f n).
proof: Proof. intros X R f p. induction p. intro k. exists (S k). exists k. auto with arith. intro k. remember (H0 (f k) (S k)). clear Heqe. destruct e as (n,e). destruct e as (m,e). destruct e. destruct H2. destruct H3. exists n. exists m. auto with arith. exists m. exists k. auto with arith. Defined.
imports: Coq(Arith Relations)