proposition: Lemma odiff_pos a b: a <o b -> \0o <o (b -o a).
proof: Proof. move=> [leab bab]; move: (odiff_pr leab) => [xx eq]. by apply :ord_ne0_pos => // h; case: bab; rewrite eq h (osum0r (proj31 leab)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)