proposition: Remark R0: exists (n:nat), (x <= (s n))%O.
proof: Proof. case Hlim => _ [H H']; apply H'; by case Hsucc. Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)