proposition: Lemma bound_lexx c1 c2 x : (BSide c1 x <= BSide c2 x) = (c2 ==> c1).
proof: Proof. by rewrite /<=%O /= lteifxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)