proposition: Lemma ap_limit x: T2ap x -> (x == one) || (T2limit x).
proof: Proof. case: x => // a b n f /= /andP[/eqP -> /eqP ->]. by rewrite eqxx orTb T2eqE !andbT; case: (_ && _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)