proposition: Lemma wlog_lt P : (forall x, P x x) -> (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=> rP sP hP x y; case: (ltgtP x y) => [||->] // /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)