proposition: Lemma T3lt_add2r p m n : (m + p < n + p ) -> (m < n).
proof: Proof. elim: m p n. by move => p n; rewrite T3add0n; case: n => //;rewrite T3add0n T3ltnn. move => a _ b _ c _ n d Hd; case; first by move => u; rewrite ! T3addn0. move => a' b' c' n' d'; case. simpl;case (T3ltgtP [a, b, c] [a', b', c']) => pa /=. + by rewrite !T3ltnn. + by rewrite T3lt_consE (T3lt_anti pa) (T3lt_ne' pa). + by rewrite T3lt_consE pa T3ltnn eqxx ltn_simpl1 eqn_simpl1. move => a'' b'' c'' n'' d'' /= h1; rewrite T3lt_consE; move: h1. case (T3ltgtP [a,b,c] [a',b',c']);case (T3ltgtP [a',b',c'] [a'',b'',c'']) => pb pa /=; rewrite T3lt_consE. - by rewrite (T3lt_trans pa pb). - by rewrite ! T3ltnn ltnn eqxx if_same. - by rewrite -pb pa. - case: (T3ltgtP [a,b,c] [a'',b'',c'']) => //. by case: (ltngtP n n'') => // _ _; apply: Hd. - by rewrite (T3lt_anti pa) (T3lt_ne' pa). - by rewrite - pb (T3lt_anti pa) (T3lt_ne' pa). - by rewrite pa pb. - by rewrite pa T3ltnn eqxx ltn_simpl1 eqn_simpl1. - by rewrite pa pb !T3ltnn eqxx ltnS ltn_add2r if_same if_simpl => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)