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