proposition: Lemma OTorder_le_alt2P r r': r <=t r' <-> [/\ order_type r, order_type r' & r <=O r'].
proof: Proof. split; first by move /OTorder_le_altP => [pa pb /order_le_alt3P pc]. by move => [pa pb /order_le_alt3P pc]; apply /OTorder_le_altP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)