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