proposition: Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}.
proof: Proof. move=> [[[] x|[]] [[] y|[]]] /neitvP //; rewrite /Rhull /= !(in_itv, inE)/= ?bnd_simp => xy. - rewrite asboolT// inf_itv// lexx/= xy asboolT// asboolT//=. by rewrite asboolF//= sup_itv//= ltxx ?andbF. - by rewrite asboolT// inf_itv// ?asboolT// ?sup_itv// ?lexx ?xy. - by rewrite asboolT//= inf_itv// lexx asboolT// asboolF. - rewrite asboolT// inf_itv//= ltxx asboolF// asboolT//. by rewrite sup_itv// ltxx andbF asboolF. rewrite asboolT // inf_itv // ltxx asboolF // asboolT //. by rewrite sup_itv // xy lexx asboolT. - by rewrite asboolT // inf_itv// ltxx asboolF // asboolF. - by rewrite asboolF // asboolT // sup_itv// ltxx asboolF. - by rewrite asboolF // asboolT // sup_itv// lexx asboolT. - by rewrite asboolF // asboolF. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences