proposition: Lemma wlog_le P : (forall x y, P y x -> P x y) -> (forall x y, x <= y -> P x y) -> forall x y, P x y.
proof: Proof. by move=> sP hP x y; case: (leP x y) => [| /ltW] /hP // /sP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)