proposition: Lemma T3lt_psi a b c a' b' c': [a,b,c] < [a', b',c'] = lt_psi a b c a' b' c'.
proof: Proof. by rewrite {1} T3ltE /lt_rec ltnn if_same if_simpl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)