proposition: Lemma lt_le a b : (forall x, x < a -> x < b) -> a <= b.
proof: Proof. move=> ab; apply/ler_addgt0Pr => e e_gt0; rewrite -lerBDr ltW//. by rewrite ab// ltrBlDr ltrDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)