proposition: Lemma OT_prop4 x: order x -> order_type_of (order_type_of x) = order_type_of x.
proof: Proof. move => ox. by apply: order_type_unique; apply: orderIS; apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)