proposition: Lemma led_mul2l c : {homo *%R c : a b / a <= b }.
proof: Proof. by move=> a b; rewrite le_def => /eqP <-; rewrite mulrDr led_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop ssralg)