proposition: Lemma sec_binary_infinite_chain : forall (X:Type) (p : WFT X) R (f : nat -> X) (k : nat), SecureBy R p -> exists n, exists m, (n > m) /\ (m >= k) /\ R (f m) (f n).
proof: Proof. intro X. intro p. induction p. intros. simpl in H. exists (S k). exists k. split. auto. split. auto. apply H. intros. simpl in H0. remember (H0 (f k)) as G. destruct (H _ _ f (S k) G). destruct H1. destruct H1. destruct H2. destruct H3. exists x. exists x0. split. apply H1. split. auto. auto with arith. apply H3. exists x0. exists k. split. auto with arith. split. auto. apply H3. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)