proposition: Lemma add_le1 a b: a <= a + b.
proof: Proof. elim:a b; first by rewrite /T3le /=; case;[ rewrite eqxx | ]. move => a' _ b' _ c' _ n' d' hd [] // a b c n d/=. case: (T3ltgtP [a', b', c'] [a, b, c]) => h; rewrite /T3le T3lt_consE. + by rewrite h orbT. + by rewrite T3ltnn ltnn T3eqE !eqxx /=; apply: hd. + by rewrite T3ltnn ltnS leq_addr eqxx orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)