proposition: Lemma Cantor_eta_prop2 r: eta_like r -> order_type_of r = Cantor_eta.
proof: Proof. move => ra. apply: order_type_unique; apply: (Cantor_eta_pr ra eta_likeQp_int01). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)