proposition: Lemma add_le1 a b: a <= a + b.
proof: Proof. elim:a b; first by rewrite /T1le /=; case;[ rewrite eqxx | ]. move => a' _ n' b' Hb [] // a n b /=. case: (T1ltgtP a' a) => h;rewrite T1le_consE ?h // ? ltnn T1ltnn !eqxx //=. by rewrite ltnS leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)