proposition: Lemma leifD x1 y1 C1 x2 y2 C2 : x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> x1 + x2 <= y1 + y2 ?= iff C1 && C2.
proof: Proof. rewrite -(mono_leif (C := C1) (lerD2r x2)). rewrite -(mono_leif (C := C2) (lerD2l y1)). exact: leif_trans. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)