proposition: Remark R1: exists z, (x < z < y)%O.
proof: Proof. case R0 => n Hn. exists (s (S n)). apply /andP; split. apply Order.POrderTheory.le_lt_trans with (s n) => //. case: Hlim => H H0. apply: H => //. case: Hlim => _ [H'' _] //. Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)