proposition: Lemma leifP x y C : reflect (x <= y ?= iff C) (if C then x == y else x < y).
proof: Proof. rewrite /leif le_eqVlt; apply: (iffP idP)=> [|[]]. by case: C => [/eqP->|lxy]; rewrite ?eqxx // lxy lt_eqF. by move=> /orP[/eqP->|lxy] <-; rewrite ?eqxx // lt_eqF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)