proposition: Lemma ap_pr4 x: (forall b, b < x -> b + x = x) -> (x == zero) || T3ap x.
proof: Proof. case: x => // a b c /=; case => [d H|]. move: (H [ a, b, c]). rewrite /= T3ltnn psi_lt2 /= T3lt0n; case:eqP => //=. by move => _ /(_ erefl). move => n d H /=. move: (H (cons a b c n zero)). rewrite /= T3lt_consE T3ltnn eqxx ltnS leqnn. by move => /(_ erefl); case => /eqP; rewrite - {3} (addn0 n) eqn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)