proposition: Lemma T2le_add2l p m n : (p + m <= p + n) = (m <= n).
proof: Proof. elim:p m n => // a _ b _ n c Hc. case; first by move => n1; rewrite T2addn0 T2le0n add_le1. move => a' b' n' c'; case. rewrite T2addn0 /=;case: (T2ltgtP [a, b] [a', b']) => h. + rewrite T2le_consE -T2lt_psi (T2lt_anti h) T2len0 ifF //. case ha: ((a' == a) && (b' == b)) => //. by move:h; case /andP: ha => /eqP -> /eqP ->; rewrite T2ltnn. + rewrite T2le_consE /lt_psi !T2ltnn !eqxx ltnn /=. by rewrite -{2} (T2addn0 c) Hc. + rewrite !T2le_consE /lt_psi !T2ltnn !eqxx /= addnC ltn_simpl1 eqn_simpl1. by rewrite T2len0. move => a'' b'' n'' c'' /=. 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'']) =>// pa pb; rewrite T2le_consE [in RHS] T2le_consE - !T2lt_psi. - move: (T2lt_trans pa pb) => pc. by rewrite ha hb (T2lt_anti pb) (T2lt_ne' pb) (T2lt_ne' pc) (T2lt_anti pc). - by rewrite ha hb -pa (T2lt_ne' pb) (T2lt_anti pb). - by rewrite (T2lt_trans pb pa) pa. - by rewrite !eqxx T2ltnn ltnn Hc T2le_consE -T2lt_psi /= hb. - by rewrite T2ltnn -pa pb !eqxx ltnS leq_addr. - by rewrite -pb pa. - rewrite T2ltnn -pb addnC ltn_simpl1 eqn_simpl1 !eqxx hb - pb. by rewrite (T2lt_anti pa) (T2lt_ne' pa). - by rewrite hb - pa pb !eqxx T2ltnn /= ltnS ltn_add2l - !addSn eqn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)