proposition: Lemma OT_opposite3 a: order a -> OT_opposite (order_type_of a) = OT_opposite a.
proof: Proof. move => oa. by apply: order_type_unique; apply:OT_opposite1; apply:OT_prop0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)