proposition: Lemma ap_pr2 c: T1nf c -> c <> zero -> (forall a b, T1nf a -> T1nf b -> a < c -> b < c -> a + b < c) -> T1ap c.
proof: Proof. case: c => // a n b nc _ Hr. have {Hr} H: forall u, T1nf u -> u < cons a n b -> u + u < cons a n b. by move => u ua ub; apply: Hr. case: n b H nc => [b H /T1nf_consa na | n b H nc]. have nc: T1nf (cons a 0 zero) by rewrite /= andbT. move: (H _ nc); rewrite /= T1ltnn eqxx /= if_same T1ltnn. by case b => // u v w; apply. have l2: (cons a n b) < (cons a n.+1 b) by rewrite /= T1ltnn eqxx ltnSn. move: (H (cons a n b) nc l2). by rewrite /= T1ltnn /= !T1ltnn /= eqxx if_same ltnS -{3}(add0n n) ltn_add2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)