proposition: Lemma smallest_setring : setring <<r G >>.
proof: Proof. split=> [|A B GA GB|A B GA GB] P [[P0 PU PDI]] GP //. by apply: (PU); [apply: GA|apply: GB]. by apply: (PDI); [apply: GA|apply: GB]. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)