proposition: Lemma led_add2r c : {homo +%R^~ c : a b / a <= b }.
proof: Proof. move => a b; rewrite !le_def => /eqP abb. by rewrite addrCA -addrA adddd addrA [b + a]addrC abb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop ssralg)