proposition: Lemma T3lt_psi_a a b c: a < [a,b,c].
proof: Proof. move: a b c. suff: forall x a b c, (x <= a -> x < [a,b,c]). by move => H a b c; apply:H; rewrite T3lenn. 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; case => // 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] ha. move: (leq_trans pb ln) (leq_trans pc ln) => la lb. move: (T3le_trans (T3le_psi a' b' c' n' d') ha) => aux. have sc: (a' < [a',b',c']) by apply:(Hrec a' (leq_trans pa ln));rewrite T3lenn. rewrite psi_lt1 T3lt_psi /lt_psi. move: (T3lt_le_trans sc aux) => sc'. rewrite sc' (T3lt_anti sc') (T3lt_ne sc') /=. have sa: (b' < [a',b',c']) by apply: T3lt_psi_b. have sb: (c' < [a',b',c']) by apply: T3lt_psi_c. rewrite (Hrec b' la) ? (T3ltW (T3lt_le_trans sa aux))//. rewrite (Hrec c' lb) ? (T3ltW (T3lt_le_trans sb aux))//. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)