proposition: Lemma ap_pr2 c: T3nf c -> c <> zero -> (forall a b, T3nf a -> T3nf b -> a < c -> b < c -> a + b < c) -> T3ap c.
proof: Proof. case: c => // a b c n d nd _ Hr. have {Hr} H: forall u, T3nf u -> u < cons a b c n d -> u + u < cons a b c n d. by move => u ua ub; apply: Hr. case: n d H nd => [d H | n d H]. rewrite /T3nf -/T3nf => /and5P[na nb nc nd ne]. have np: T3nf [a,b,c] by rewrite nf_psi na nb nc. move: (H _ np). rewrite T3lt_consE T3ltnn eqxx /= T3ltnn T3lt_consE T3ltnn eqxx /= T3lt0n. by case: eqP => // _; apply. have l2: (cons a b c n d) < (cons a b c n.+1 d) by rewrite psi_lt2 ltnS leqnn. move=> pa; have pb: T3nf (cons a b c n d) by move: pa; rewrite /T3nf -/T3nf. move: (H _ pb l2); rewrite /= T3ltnn psi_lt2 T3ltnn ltnS if_same. by rewrite -{3}(add0n n) ltn_add2r /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)