proposition: Lemma T1le_add2r p m n : (m <=n) -> (m + p <= n + p).
proof: Proof. rewrite !T1leNgt; apply: contra; apply: T1lt_add2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)