proposition: Lemma is_pos_div_2 (eps : posreal) : 0 < eps / 2.
proof: Proof. unfold Rdiv ; apply Rmult_lt_0_compat ; [apply eps | apply Rinv_0_lt_compat, Rlt_0_2]. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)