proposition: Lemma T1le_add2l p m n : (p + m <= p + n) = (m <= n).
proof: Proof. elim:p m n => // a Ha n b Hb. case; first by move => n1; rewrite T1addn0 T1le0n add_le1. move => a' n' b'; case. rewrite T1addn0 /=; case (T1ltgtP a a'). move => h; rewrite T1le_consE (T1lt_ne' h) (T1lt_anti h) => //. move: (Hb (cons a' n' b') zero). by rewrite T1le_consE T1addn0 T1ltnn ltnn ! eqxx => ->. by rewrite T1le_consE T1ltnn eqxx addnC ltn_simpl1 eqn_simpl1. move => a'' n'' b'' /=. case (T1ltgtP a a');case (T1ltgtP a a'') =>// pa pb; rewrite ? pa -? pa !T1le_consE ? (T1lt_anti pb) ? eqxx ? T1ltnn. - move: (T1lt_trans pa pb) => pc. by rewrite (T1lt_ne' pb) (T1lt_ne' pc) (T1lt_anti pc). - by rewrite (T1lt_ne' pb). - by rewrite pa (T1lt_trans pb pa). - by rewrite Hb ltnn T1le_consE. - by rewrite pb ltnS leq_addr. - by rewrite -pb pa. - by rewrite -pb addnC ltn_simpl1 eqn_simpl1 (T1lt_anti pa) (T1lt_ne' pa). - by rewrite pb eqxx T1ltnn /= ltnS ltn_add2l - !addSn eqn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)