proposition: Lemma contra_le_not P x y : (P -> x < y) -> (y <= x -> ~ P).
proof: Proof. by case: comparableP => // _ PF _ /PF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)