proposition: Lemma odiff_pr1_wrong a: omega0 <=o a -> (a +o \1o) -o \1o <> a.
proof: Proof. move => h. have op:= proj32 h. move: (oltS op) => [l1 /nesym l2]. by rewrite (osucc_pr op) (odiff_1inf (oleT h l1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)