proposition: Lemma gt0_clamp {R : realType} (e : R) : 0 < eclamp e.
proof: Proof. by rewrite /eclamp; case: (lerP e 0) => h //; apply/ltr01. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology