proposition: Lemma T3lt_psi_bc a b c: ((b < [a,b,c]) && (c < [a, b, c])).
proof: Proof. move: a b c. suff: forall x a b c, ((x <= b) || (x <= c)) -> x < [a,b,c]. by move => H a b c; apply/andP; split; apply:H; rewrite T3lenn // orbT. move => x; set n := (size x).+1. move: (leqnn n); rewrite {1}/n;move: n. move => n; elim: n x; first by move => x //;rewrite ltn0. move => m Hrec [] // a' b' c' n' d'; rewrite ltnS => ln. move => a b c. move: (size_prop1 a' b' c' n' d'); set x := (cons a' b' c' n' d'). move /and5P=> [pa pb pc pd pe]. move: (leq_trans pb ln) (leq_trans pc ln) => la lb. have sa: (b' < [a',b',c']) by apply: (Hrec b' la); rewrite T3lenn. have sb: (c' < [a',b',c']) by apply: (Hrec c' lb); rewrite T3lenn orbT. case /orP => ha. rewrite T3lt_consE; apply: ifT; rewrite /lt_psi. have aux := (T3le_trans (T3le_psi a' b' c' n' d') ha). move: (T3lt_le_trans sa aux) (T3lt_le_trans sb aux) => sa' sb'. have sc: (b' < [a,b,c]) by apply:(Hrec b' la); rewrite (T3ltW sa'). have sd: (c' < [a,b,c]) by apply:(Hrec c' lb);rewrite (T3ltW sb'). move: aux; rewrite /T3le orbC => aux. rewrite T3lt_psi /lt_psi sa' sc sd /=. by case: (T3ltgtP a' a) => //; rewrite ?orbT //= orbA aux. rewrite T3lt_consE; apply: ifT; rewrite /lt_psi. have aux:= (T3le_trans (T3le_psi a' b' c' n' d') ha). move: (T3lt_le_trans sa aux) (T3lt_le_trans sb aux) => sa' sb'. have sc: (b' < [a,b,c]) by apply:(Hrec b' la); rewrite (T3ltW sa') orbT. have sd: (c' < [a,b,c]) by apply:(Hrec c' lb); rewrite (T3ltW sb') orbT. move: aux; rewrite /T3le orbC => aux. rewrite T3lt_psi /lt_psi sb' sc sd /=. case: (T3ltgtP a' a) => //=; first by rewrite aux !orbT. by case: (T3ltgtP b' b) => //=; rewrite orbF aux. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)