proposition: Lemma odiff_wrong a b: b <=o a -> b -o a = \0o.
proof: Proof. move => ba; move: (ba) => [ob oa _]; apply /set0_P. move => t /Zo_P [tb /(oltP ob) s1]. exact: (oltNge (olt_leT s1 ba) (osum_Mle0 oa (Os_ordinal ob tb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)