proposition: Lemma OT_nat_1 : OT_of_nat \1o = \1t.
proof: Proof. congr (order_type_of _). set_extens t. move=> /Zo_S /setX_P[p /set1_P ha /set1_P hb]. by apply/set1_P;rewrite - p ha hb. move => /set1_P ->; apply: Zo_i; last by aw. by apply: setXp_i; apply: set1_1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)