proposition: Lemma leq_div2l m d e : 0 < d -> d <= e -> m %/ e <= m %/ d.
proof: Proof. move/leq_divRL=> -> le_de. by apply: leq_trans (leq_trunc_div m e); apply: leq_mul. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)