proposition: Lemma ltn_add_ll m1 m2 n1 n2: m1 < n1 -> m2 < n2 -> m1 + m2 < n1 + n2.
proof: Proof. by move => pa pb; exact: (ltn_add_el (ltnW pa) pb). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)