proposition: Lemma expand_eqoo r : (expand r == +oo) = (1 <= r)%R.
proof: Proof. by rewrite /expand; case: ifP => //; case: ifP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed