proposition: Lemma prod_lt_eps0 a n: a <o epsilon0 -> natp n -> a *o n <o epsilon0.
proof: Proof. move => ae nN; move:(proj31_1 ae) => oa. move: n nN; apply:Nat_induction. rewrite oprod0r; exact: (ole_ltT (ole0x oa) ae). move => n nN Hrec. rewrite (succ_of_nat nN) (oprod2_succ oa (OS_nat nN)). apply: (sum_lt_eps0 Hrec ae). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)