proposition: Lemma T2lt_add2r p m n : (m + p < n + p ) -> (m < n).
proof: Proof. elim: m p n. by move => p n; rewrite T2add0n; case: n => //;rewrite T2add0n T2ltnn. move => a _ b _ n c Hc; case; first by move => u; rewrite ! T2addn0. move => a' b' n' c'; case. simpl;case (T2ltgtP [a, b] [a', b']) => pa /=. + by rewrite !T2ltnn. + have h:(a == a') &&(b== b') = ([a,b] == [a',b']) by rewrite T2eqE !andbT. by rewrite T2lt_consE -T2lt_psi h (T2lt_anti pa) (T2lt_ne' pa). + case: pa => -> ->. by rewrite T2lt_consE -T2lt_psi T2ltnn !eqxx ltn_simpl1 eqn_simpl1. move => a'' b'' n'' c'' /= h1; rewrite T2lt_consE; move: h1. have ha:(a == a'') &&(b== b'') = ([a,b] == [a'',b'']) by rewrite T2eqE !andbT. have hb:(a == a') &&(b== b') = ([a,b] == [a',b']) by rewrite T2eqE !andbT. case (T2ltgtP [a,b] [a',b']);case (T2ltgtP [a',b'] [a'',b'']) => pb pa /=; rewrite T2lt_consE - !T2lt_psi // ? ha ? hb. - by rewrite (T2lt_trans pa pb). - by rewrite ! T2ltnn ltnn !eqxx //. - by rewrite -pb pa. - case: (T2ltgtP [a,b] [a'',b'']) => //. by case: (ltngtP n n'') => // _ _ ; apply: Hc. - by rewrite (T2lt_anti pa) (T2lt_ne' pa). - by rewrite - pb (T2lt_anti pa) (T2lt_ne' pa). - by rewrite pa pb. - by rewrite pa T2ltnn eqxx ltn_simpl1 eqn_simpl1. - by rewrite pa pb !T2ltnn eqxx ltnS ltn_add2r if_same if_simpl => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)