proposition: Lemma psi_succ_pr1 a b c: [a,b,c] < psi_succ ([a,b,c]).
proof: Proof. simpl; case ha: ((a== zero) && (b==zero)); last by apply: T3lt_psi_c. move/andP:ha => [/eqP -> /eqP ->]. by rewrite lt_omega2 eqxx succ_lt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)