proposition: Lemma prod_entourage : entourage = entourage_ prod_ball.
proof: Proof. rewrite predeqE => P; split; last first. move=> [_/posnumP[e] sbeP]. exists ([set xy | ball xy.1 e%:num xy.2], [set xy | ball xy.1 e%:num xy.2]) => //=. move=> [[a b] [c d]] [bab bcd]; exists ((a, c), (b, d))=> //=. exact: sbeP. move=> [[A B]] /=; rewrite -!entourage_ballE. move=> [[_/posnumP[eA] sbA] [_/posnumP[eB] sbB] sABP]. exists (Num.min eA eB)%:num => //= -[[a b] [c d] [/= bac bbd]]. suff /sABP [] : (A `*` B) ((a, c), (b, d)) by move=> [[??] [??]] ? [<-<-<-<-]. split; [apply: sbA|apply: sbB] => /=. by apply: le_ball bac; rewrite num_le le_minl lexx. by apply: le_ball bbd; rewrite num_le le_minl lexx orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed