proposition: Lemma osuccNpred x: osuccp x -> x = opred x -> False.
proof: Proof. move => [y oy yt] xv; case: (nesym (proj2 (oltS oy))). by move: (succo_K oy); rewrite - yt - xv yt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)