proposition: Lemma mul_itv_boundrC_subproof b1 b2 : mul_itv_boundr_subdef b1 b2 = mul_itv_boundr_subdef b2 b1.
proof: Proof. by move: b1 b2 => [[] [[|?]|?] | []] [[] [[|?]|?] | []] //=; rewrite mulnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(interval) mathcomp(mathcomp_extra boolp) signed