proposition: Lemma oprec_nat2 n: \0o <o n -> n <o omega0 -> (osucc n -o \1o) = osucc (n -o \1o).
proof: Proof. move => xz cox. have ox:= proj32_1 xz. have xb: inc n omega0 by case/oltP0: cox. rewrite -(oprec_nat xz cox);symmetry;apply:(odiff_pr2 OS1 (OS_succ ox) ox). by rewrite (osum2_2int NS1 xb) csumC -(osum2_2int xb NS1) (osucc_pr ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)