proposition: Lemma interval_signP l u : interval_sign_spec l u (interval_sign (Interval l u)).
proof: Proof. rewrite /interval_sign/itv_bound_signl/itv_bound_signr. have [lneg|lpos|->] := ltgtP l; have [uneg|upos|->] := ltgtP u. - apply: ISignNeg => //; exact: ltW. - exact: ISignBoth. - exact: ISignNeg. - by apply/ISignNone/ltW/(lt_le_trans uneg); rewrite leBRight_ltBLeft. - by apply: ISignPos => //; exact: ltW. - by apply: ISignNone; rewrite leBRight_ltBLeft. - by apply: ISignNone; rewrite -ltBRight_leBLeft. - exact: ISignPos. - exact: ISignEqZero. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed