proposition: Corollary af_inf_chain (X : Type) (R : X -> X -> Prop): almost_full R -> forall (f : nat -> X), exists n, exists m, (n > m) /\ R (f m) (f n).
proof: Proof. intros. destruct (@sec_binary_infinite_chain X R f H 0); firstorder. Defined.
imports: Coq(Arith Relations)