proposition: Lemma expandN1 r : (r <= -1)%R -> expand r = -oo.
proof: Proof. by rewrite lerNr => /expand1/eqP; rewrite expandN eqe_oppLR => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed