proposition: Lemma succ_psi1 a b c (x:= [a, b, c]): ((a != zero) || (b != zero)) -> (forall a' b' c', x < [a',b',c'] -> (psi_succ x) <= [a',b',c']).
proof: Proof. move => sab. rewrite {2}/x /psi_succ -(negbK ((a == zero) && (b == zero))) negb_and sab /=. move => a' b' c' ee; move: (ee). rewrite /T3le !T3lt_psi /lt_psi !T3ltn0 !T3lt0n andbF /= ee. move: sab. case az: (a'==zero) => //; rewrite ?orbT // (eq_sym zero a') az /=. rewrite (eqP az) T3ltn0 T3lt0n T3eqE (eq_sym zero b'). case az': (a==zero) => //=; case bz': (b'==zero) => //=; rewrite (eqP bz') //. rewrite T3ltn0 T3lt0n eqxx !orbF; case bz: (b==zero) => //=. by rewrite orbC andbT. by rewrite /= orbC eqxx andbT orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)