proposition: Lemma T1lt_add2r p m n : (m + p < n + p ) -> (m < n).
proof: Proof. elim: m p n. by move => p n; rewrite T1add0n; case: n => //;rewrite T1add0n T1ltnn. move => a Ha n b Hb; case; first by move => u; rewrite ! T1addn0. move => a' n' b'; case. simpl;case (T1ltgtP a a') => pa /=. + by rewrite !T1ltnn ltnn !if_same. + by rewrite (T1lt_anti pa) (T1lt_ne' pa). + by rewrite pa T1ltnn eqxx ltn_simpl1 eqn_simpl1. move => a'' n'' b'' /=. case (T1ltgtP a a'); case (T1ltgtP a a'') => pa pb //. - by rewrite (T1lt_trans pa pb) T1ltnn. - by rewrite -pa pb T1ltnn. - case (T1ltgtP a'' a') => pc /=; rewrite ? pc. + by rewrite (T1lt_anti pb) (T1lt_ne' pb). + by rewrite (T1lt_anti pa) (T1lt_ne' pa). + by rewrite (T1lt_anti pb) (T1lt_ne' pb). - rewrite - pa pb (T1lt_anti pb) /= T1ltnn eqxx. by case (ltngtP n n'') => // _; apply: Hb. - by rewrite - pb pa /= T1ltnn eqxx ltn_simpl1 eqn_simpl1. - by rewrite -pa -pb /= !T1ltnn eqxx ltnS ltn_add2r if_same if_simpl=> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)