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