proposition: Lemma add_le1 a b: a <= a + b.
proof: Proof. elim:a b; first by rewrite /T2le /=; case;[ rewrite eqxx | ]. move => a' _ b' _ n' c' hc [] // a b n c /=. case: (T2ltgtP [a', b'] [a, b]) => h; rewrite T2le_consE -T2lt_psi ?T2ltnn. + by rewrite h. + by rewrite !eqxx ltnn /=; apply: hc. + by rewrite !eqxx ltnS leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)