proposition: Lemma ap_pr1 c: (forall a b, a < c -> b < c -> a + b < c) -> (c== zero) || T2ap c.
proof: Proof. case: c => // a b n c /=. case: n c => [d H | n c H]; last first. have l2: (cons a b n c) < (cons a b n.+1 c) by rewrite psi_lt2 ltnS leqnn. move: (H _ _ l2 l2). rewrite /= psi_lt2 /= psi_lt2 /= T2ltnn if_same ltnS. by rewrite -{3}(add0n n) ltn_add2r. case dz: (d == zero) => //. have pa: [a,b] < cons a b 0 d by rewrite psi_lt2 /= T2lt0n dz. by move: (H _ _ pa pa); rewrite /= psi_lt2 /= psi_lt2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)