proposition: Lemma osum_1inf a: omega0 <=o a -> \1o +o a = a.
proof: Proof. move => pa; move: (odiff_pr pa) => [pb pc]; rewrite pc. by rewrite (osumA OS1 OS_omega pb) (osum_int_omega olt_1omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)