proposition: Lemma Cantor_eta_pr1: order_type_of Nat_order <> Cantor_eta.
proof: Proof. move:Nat_order_wor => [[or _] sr]. move/(Cantor_etaP or) => [[_ _ h _ _] _]. by rewrite sr in h; move:(h _ NS0) => [y [/Nat_order_leP[_ _ /cle0 h3]]]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)