proposition: Lemma T3lt_psi' a b c a' b' c': [a, b, c] < [a', b', c' ] = [|| [&& a==a', b==b' & c < c'], [&& a==a', b < b' & c < [a', b', c'] ], [&& a==a', b' <b & [a,b,c] <= c'], [&& a < a', b < [a', b', c'] & c < [a', b', c']], ((a' < a) && ([a,b,c] <= b')) | ((a' < a) && ([a,b,c] <= c'))].
proof: Proof. rewrite T3lt_psi /lt_psi; case: (T3ltgtP a a') => //=. by rewrite orbA (orbC (_ < b')) -/(T3le _ _) (orbC (_ < c')) -/(T3le _ _). case: (T3ltgtP b b') => //=. by rewrite !orbF orbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)