proposition: Lemma add_le2 a b: b <= a + b.
proof: Proof. case: a => // a' n' b'; case: b ; [done | move => a n b /=]. case: (T1ltgtP a' a) => // h;rewrite T1le_consE ?h // ltnS leq_addl /= eqxx. by rewrite if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)