fact: Definition le x y := (tag x <= tag y) && ((tag x >= tag y) ==> (tagged x <= tagged_as x y)).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)