proposition: Lemma oprec_nat n: \0o <o n -> n <o omega0 -> n = osucc (n -o \1o).
proof: Proof. move => xnz xo. have pa: \1o <=o n by apply/ oge1P. have [sa sb]:= (odiff_pr pa). move: (osum_M0le OS1 sa); rewrite - sb => sc; move: (ole_ltT sc xo) => yo. have sd: inc (n -o \1o) omega0 by case/oltP0: yo. rewrite - (osucc_pr sa) {1} sb. by rewrite (osum2_2int NS1 sd) (osum2_2int sd NS1) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)