proposition: Lemma lteif_anti C1 C2 x y : (x < y ?<= if C1) && (y < x ?<= if C2) = C1 && C2 && (x == y).
proof: Proof. by case: C1 C2 => [][]; rewrite lte_anti. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)