proposition: Lemma lteifNF x y C : y < x ?<= if ~~ C -> x < y ?<= if C = false.
proof: Proof. by case: C => [/lt_geF|/le_gtF]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)