proposition: Lemma T3le_add2l p m n : (p + m <= p + n) = (m <= n).
proof: Proof. elim:p m n => // a _ b _ c _ n d Hd. case; first by move => n1; rewrite T3addn0 T3le0n add_le1. move => a' b' c' n' d'; case. rewrite T3addn0 /=; case: (T3ltgtP [a, b, c] [a', b', c']) => h. by rewrite T3le_consE (T3lt_ne' h) (T3lt_anti h) T3len0. by rewrite T3le_consE T3ltnn ltnn !eqxx - (Hd _ zero) T3addn0. by rewrite T3le_consE T3ltnn eqxx addnC ltn_simpl1 eqn_simpl1 T3len0. move => a'' b'' c'' n'' d'' /=. case: (T3ltgtP [a, b, c] [a', b', c']);case:(T3ltgtP [a, b, c] [a'', b'', c'']) =>// pa pb; rewrite T3le_consE [in RHS] T3le_consE. - move: (T3lt_trans pa pb) => pc. by rewrite (T3lt_anti pb) (T3lt_ne' pb) (T3lt_ne' pc) (T3lt_anti pc). - by rewrite -pa (T3lt_ne' pb) (T3lt_anti pb). - by rewrite (T3lt_trans pb pa) pa. - by rewrite !eqxx T3ltnn ltnn Hd T3le_consE. - by rewrite T3ltnn -pa pb eqxx ltnS leq_addr. - by rewrite -pb pa. - rewrite T3ltnn -pb addnC ltn_simpl1 eqn_simpl1 eqxx. by rewrite (T3lt_anti pa) (T3lt_ne' pa). - by rewrite - pa pb eqxx T3ltnn /= ltnS ltn_add2l - !addSn eqn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)