proposition: Lemma add_le2 a b: b <= a + b.
proof: Proof. case: a => // a' b' n' c'; case: b ; [done | move => a b n c /=]. case: (T2ltgtP [a', b'] [a, b]) => h; rewrite T2le_consE -T2lt_psi ?h => //. + by rewrite !eqxx /= ltnn T2lenn if_same. + by case: h => -> ->; rewrite T2ltnn ltnS leq_addl !eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)