proposition: Theorem T3lt_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 T3ltn0 | move => a b c n d; case]. move => a b c n d []; [ by rewrite T3ltn0 | move => a' b' c' n' d']. case; [ by rewrite T3ltn0 | move => a'' b'' c'' n'' d'']; rewrite ltnS => la. have Hr1: forall v u w, (size u < size (cons a b c n d))%N -> (size v <= size (cons a' b' c' n' d'))%N -> (size w <= size (cons a'' b'' c'' n'' d''))%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. have Hr2: forall v u w, (size u <= size (cons a b c n d))%N -> (size v < size (cons a' b' c' n' d'))%N -> (size w <= size (cons a'' b'' c'' n'' d''))%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_el. have Hr3: forall v u w, (size u <= size (cons a b c n d))%N -> (size v <= size (cons a' b' c' n' d'))%N -> (size w < size (cons a'' b'' c'' n'' d''))%N -> u < v -> v < w -> u < w. move => u v w sa sb sc; apply: Hrec; apply: leq_trans la. by rewrite ltn_add_el // leq_add. move: (size_prop1 a b c n d) => /and5P [pa pb pc pd pe]. move: (size_prop1 a' b' c' n' d') => /and5P [pa' pb' pc' pd' pe']. move: (size_prop1 a'' b'' c'' n'' d'') => /and5P [pa'' pb'' pc'' pd'' pe'']. rewrite T3lt_consE (T3lt_consE a') (T3lt_consE a _ _ _ _ a''). case (T3ltgtP [a, b, c] [a', b', c']) => //; last first. move => <-; case (T3ltgtP [a, b, c] [a'', b'', c'']) => //. move => _; case (ltngtP n n') => //. move => nn'; case (ltngtP n' n'') =>//. by move => nn''; rewrite (ltn_trans nn' nn''). by move => <-; rewrite nn'. by move => <- dd'; case (ltngtP n n'') => // _ dd''; rewrite (Hr1 d') // ltnW. move => lta _; case (T3ltgtP [a', b', c'] [a'', b'', c'']) => //; last first. by move => <-; rewrite lta. move => ltb _; apply: ifT. move: (lta) (ltb); rewrite !T3lt_psi /lt_psi. case (T3ltgtP a a') => qa. + rewrite /= !orbF => /andP [lx ly]. have ha: [a,b,c] < [a',b',c'] by rewrite T3lt_psi /lt_psi qa lx ly !orbT. case: (T3ltgtP a' a'') => qb. - rewrite /= !orbF => /andP [lz lt]. rewrite (Hr1 a' a a'' pa (ltnW pa') (ltnW pa'') qa qb). rewrite (Hr1 [a', b', c'] b [a'', b'', c''] pb pe' pe'' lx ltb). by rewrite (Hr1 [a', b', c'] c [a'', b'', c'']) // !orbT. - move => /= h; case: (T3ltgtP a'' a) => qc. * rewrite (T3lt_ne' qc) /=; case/or4P:h => h. + by rewrite (Hr3 [a', b', c']). + by rewrite - (eqP h) ha. + by rewrite (Hr3 [a', b', c'] [a,b,c] c'') ?orbT. + by rewrite - (eqP h) ha !orbT. * rewrite (T3lt_ne qc) /= orbF. by rewrite (Hr1 _ _ _ pb pe' pe'' lx ltb) (Hr1 _ _ _ pc pe' pe'' ly ltb). * rewrite qc eqxx /= -qc (Hr1 _ _ _ pc pe' pe'' ly ltb). move: h; case: (T3ltgtP [a', b', c'] b'') => h; last 1 first. by rewrite - h lx !orbT. by rewrite (Hr1 _ _ _ pb pe' (ltnW pb'') lx h) orbT. rewrite /= qc => h1. have [-> ->] : [a, b, c] < c'' /\ c < c''. case /orP:h1 => h1; last by rewrite - (eqP h1). rewrite (Hr1 _ _ _ pc pe' (ltnW pc'') ly h1). by rewrite (Hr3 [a', b', c']). by rewrite !andbT; case: (T3ltgtP b b''). - have/andP [sa sb]: (b < [a'', b'', c'']) && (c < [a'', b'', c'']). by rewrite (Hr1 [a', b', c']) // (Hr1 [a', b', c']) //. by rewrite sa sb -qb qa /= !orbT. + move => /= lt1; case: (T3ltgtP a'' a') => qb. - have qc: (a'' < a). rewrite (Hrec a'' a' a) //; apply:leq_trans la. by rewrite addnC (addnC (size a'')) addnA !ltn_add_ll. rewrite qc (T3lt_anti qc) (T3lt_ne' qb) (T3lt_ne' qc) /=. case /or4P => h. * by rewrite (Hr3 [a', b', c']). * by rewrite - (eqP h) lta. * by rewrite (Hr3 [a', b', c'] [a,b,c] c'') // !orbT. * by rewrite - (eqP h) lta !orbT. - rewrite (T3lt_ne qb) /= orbF => /andP [sa sb]. rewrite -/(lt_psi a b c a'' b'' c'') -(T3lt_psi); case /or4P:lt1 => h. * by apply: (Hr2 b'). * by rewrite (eqP h). * by apply: (Hr2 c'). * by rewrite (eqP h). - rewrite qb eqxx qa (T3lt_ne' qa) (T3lt_anti qa)/= -{1} qb. case: (T3ltgtP b' b'') => qc. * rewrite /= orbF => qd; case /or4P: lt1 => lt1. + by rewrite (Hr2 b') // ltnW. + by rewrite (eqP lt1) qc. + move: (Hr2 c' [a, b, c] [a'',b'',c''] pe pc' pe'' lt1 qd). by rewrite T3lt_psi /lt_psi qb qa (T3lt_ne' qa) (T3lt_anti qa). + move: qd; rewrite -(eqP lt1) T3lt_psi /lt_psi. by rewrite qb qa (T3lt_ne' qa) (T3lt_anti qa). * rewrite /= orbF;case /orP =>h; last by rewrite - (eqP h) lta ! orbT. by rewrite (Hr3 [a', b', c'] _ c'') // !orbT. * rewrite /= orbF - qc => qd; case /or4P: lt1 => h'; rewrite ?h' ?orbT //. by rewrite (Hr2 c' _ c'') ? orbT // ltnW. by rewrite (eqP h') qd ? orbT. + rewrite - qa [in [a, b', c']] qa /=; case: (T3ltgtP a a'') => qb. - case: (T3ltgtP b b') => qc. * rewrite /= !orbF => sa /andP [sb sc]. by rewrite (Hr1 b') // ?(ltnW pb') // (Hr1 [a', b', c']). * rewrite /= !orbF => sa /andP [sb sc]. have: ([a, b, c] < [a'', b'', c'']). by case /orP: sa => h; [rewrite (Hr2 c') | rewrite (eqP h)]. rewrite T3lt_psi /lt_psi qb (T3lt_ne qb) (T3lt_anti qb) orbF //. * by rewrite /= !orbF => qd /andP [sa sb]; rewrite qc sa (Hr1 c') // ltnW. - move => sa /=; case /or4P => sc. * by rewrite (Hr3 [a',b',c']). * by rewrite - (eqP sc) lta. * by rewrite (Hr3 [a',b',c'] _ c'') // !orbT. * by rewrite - (eqP sc) lta !orbT. - case: (T3ltgtP b b') => qc /=; rewrite !orbF => qd. * case: (T3ltgtP b' b'') => qe; rewrite /= ? orbF => qf. + rewrite (Hr1 b' b b'') // ?(ltnW pb') ?(ltnW pb'') //. by rewrite (Hr1 [a', b', c'] _ [a'', b'', c'']) ? orbT. + case: (T3ltgtP b b'') => sa /=. - by rewrite (Hr1 [a', b', c']). - apply: ifT; case/orP: qf => qf; last by rewrite -(eqP qf). by apply: (Hr3 [a', b', c']). - case /orP: qf => qf; last by rewrite -(eqP qf) qd. by rewrite (Hr1 [a', b', c']) ? (ltnW pc''). + by rewrite (Hr1 [a', b', c'] c [a'', b'', c'']) // - qe qc !orbT. * case: (T3ltgtP b' b'') => qe; rewrite /= ? orbF => qf. - have: [a,b,c] < [a'',b'',c'']. by case /orP: qd =>h; rewrite ? (eqP h) // (Hr2 c'). by rewrite T3lt_psi /lt_psi qb eqxx T3ltnn /= orbF. - have ->: (b'' < b). rewrite (Hrec b'' b' b) //; apply:leq_trans la. by rewrite addnC (addnC (size b'')) addnA !ltn_add_ll. case /orP: qf => qf; last by rewrite - (eqP qf) lta !orbT. by rewrite (Hr3 [a', b', c'] [a, b, c]) // !orbT. - rewrite -qe qc /= (_: ([a, b, c] < c'')) ?orbT //. by case /orP: qd => qd; rewrite ? (eqP qd) // (Hr2 c') // ltnW. * case: (T3ltgtP b' b'') => qe /=; rewrite ? orbF => qf. - by rewrite qc qe (Hr1 c' _ [a'', b'', c'']) ? orbT // ltnW. - rewrite [in (b''< b)] qc qe /=. case /orP: qf => qf; last by rewrite - (eqP qf) lta !orbT. by rewrite (Hr3 [a', b', c'] [a, b, c]) // !orbT. - by rewrite qc qe eqxx (Hr1 c') // ltnW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)