proposition: Lemma sum_lt_eps0 a b: a <o epsilon0 -> b <o epsilon0 -> a +o b <o epsilon0.
proof: Proof. move => ae be. have h: indecomposable epsilon0. by move: epsilon0p => [pa <-]; apply: indecomp_prop4. apply:(indecomp_prop2 ae be h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)