proposition: Lemma ap_pr4 x: (forall b, b < x -> b + x = x) -> (x == zero) || T2ap x.
proof: Proof. case: x => // a b /=; case => [d H|]. move: (H [ a, b]). rewrite /= T2ltnn psi_lt2 /= T2lt0n; case:eqP => //=. by move => _ /(_ erefl). move => n d H /=. move: (H (cons a b n zero)). rewrite /= T2lt_consE -T2lt_psi T2ltnn !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)