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