proposition: Lemma led_add2l c : {homo +%R c : a b / a <= b }.
proof: Proof. move=> a b; rewrite !(addrC c); exact: led_add2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop ssralg)