proposition: Lemma OT_double_opposite x: order_type x -> OT_opposite (OT_opposite x) = x.
proof: Proof. move=> otx; rewrite /OT_opposite. have ox : order x by apply: OT_prop2. have xp1: x= order_type_of x by move: otx => [y yo yp]; rewrite yp OT_prop4 //. rewrite {2} xp1; apply: order_type_unique. rewrite -{2} (OT_opposite2 ox);apply: OT_opposite1. apply: OT_prop0; apply: (proj1 (opp_osr ox)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)