proposition: Theorem T2lt_trans b a c: a < b -> b < c -> a < c.
proof: Proof. set n := (size a + size b + size c).+1. move: (leqnn n); rewrite {1}/n; move: n. move => n; elim: n a b c; first by move => a b c//;rewrite ltn0. move => m Hrec []; first by case; [rewrite T2ltn0 | move => a' b' n' c'; case]. move => a b n c []; [ by rewrite T2ltn0 | move => a' b' n' c' ]. case; [ by rewrite T2ltn0 | move => a'' b'' n'' c'']; rewrite ltnS => la. have Hr1: forall u v w, (size u < size (cons a b n c))%N -> (size v <= size (cons a' b' n' c'))%N -> (size w <= size (cons a'' b'' n'' c''))%N -> u < v -> v < w -> u < w. move => u v w sa sb sc; apply: Hrec; apply: leq_trans la. by rewrite ltn_add_le // ltn_add_le. move: (size_prop1 a b n c) => [pa pb pc pd]. move: (size_prop1 a' b' n' c') => [pa' pb' pc' pd']. move: (size_prop1 a'' b'' n'' c'') => [pa'' pb'' pc'' pd'']. rewrite !T2lt_consE /lt_psi. case (T2ltgtP a a') => qa. + rewrite /= !orbF if_simpl => lx. case (T2ltgtP a' a'') => qb. - rewrite andTb !orbF if_simpl => qc. rewrite (Hr1 _ _ _ pb pd' pd'' lx (T2lt_psi_aux qb qc)). by rewrite (Hr1 a a' a'' pa (ltnW pa') (ltnW pa'') qa qb). - case (T2ltgtP a a'') => qc. * rewrite /= !orbF !if_simpl => qd; apply:(Hr1 _ _ _ pb pd' pd'' lx). by rewrite T2lt_psi /lt_psi qb (T2lt_anti qb) (T2lt_ne' qb) /=. * rewrite /= !if_simpl => qd. move: (T2lt_psi_aux qa lx) => ha. apply: ifT; case /orP: qd => h; last by rewrite - (eqP h). apply: (Hrec [a, b] [a', b'] b'') => //;apply: leq_trans la. by rewrite ltn_add_el // leq_add. * rewrite /= !orbF if_simpl; case /orP; last by move/eqP <-; rewrite lx. by move => qd; rewrite (Hr1 _ _ _ pb pd' (ltnW pb'') lx qd). - rewrite - qb qa (T2lt_ne qa) (T2lt_anti qa) /= !orbF !if_simpl. case (T2ltgtP b' b'') => h //=; [move => _; rewrite qb | by rewrite - h]. apply: (Hr1 _ _ _ pb pd' pd'' lx). by rewrite T2lt_psi /lt_psi qb h eqxx orbT. + case (T2ltgtP a' a'') => qb. - rewrite /= !orbF !if_simpl => sa sb; rewrite ifT//. rewrite -/(lt_psi a b a'' b'') -(T2lt_psi a b a'' b''). case/orP:sa => h; last by rewrite (eqP h). apply: (Hrec [a,b] b' [a'',b'']) => //; apply: leq_trans la. by rewrite ltn_add_le // ltn_add_el. - have qc: (a'' < a). apply: (Hrec a'' a' a) => //; apply: leq_trans la. rewrite addnAC -addnA addnC ltn_add_ll// ltn_add_ll//. rewrite /= qc (T2lt_anti qc) (T2lt_ne' qc) /= !if_simpl => r1 r2. have sa:([a,b] < [a',b']) by rewrite T2lt_psi /lt_psi qa /= -!orbA r1 !orbT. apply: ifT;case /orP: r2 => h; last by rewrite - (eqP h). apply: (Hrec [a, b] [a', b'] b'') => //;apply: leq_trans la. by rewrite ltn_add_el // leq_add. - rewrite - qb qa (T2lt_anti qa) (T2lt_ne' qa) /= ? if_simpl. case (T2ltgtP b' b'') => qc // sa sb; last by rewrite - qc. apply: ifT; case /orP: sa => h; last by rewrite (eqP h). apply: (Hrec [a,b] b' b'') => //; apply: leq_trans la. by rewrite ltn_add_ll // ltn_add_el. + rewrite -qa /= !orbF; case (T2ltgtP b b') => qb //; last first. - rewrite - qb; case (T2ltgtP a a'') => qc //=;case (T2ltgtP b b'') => //= _. case: (ltngtP n n')=> //;case:(ltngtP n' n'') => //. * by move => sa sb; rewrite (ltn_trans sb sa). * by move => -> ->. * by move => h ->; rewrite h. * move => -> -> sa sb; rewrite (Hr1 _ _ _ pc (ltnW pc') (ltnW pc'') sa sb). by rewrite ltnn eqxx. - move => _; case (T2ltgtP a a'') => qc /=; rewrite ?orbF ? if_simpl. * exact: (Hr1 _ _ _ pb (ltnW pb') pd'' qb). * have h: [a, b] < [a, b'] by rewrite T2lt_psi /lt_psi eqxx qb !orbT. move => h1;apply: ifT; case /orP: h1 => h2; last by rewrite - (eqP h2). apply: (Hrec [a, b] [a, b'] b'') => //;apply: leq_trans la. rewrite ltn_add_el // {2} qa leq_add //. * case (T2ltgtP b b'') => // h. have hh:(size b'' + size b + size b' < m)%N. by apply: leq_trans la; rewrite -addnA addnC ltn_add_ll// ltn_add_ll//. move: (Hrec b'' b b' hh h qb) => s. by rewrite (T2lt_anti s) (T2lt_ne' s). by rewrite -h (T2lt_anti qb) (T2lt_ne' qb). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)