proposition: Lemma ap_limit x: T3ap x -> (x == one) || (T3limit x).
proof: Proof. case: x => // a b c n d /= /andP[/eqP -> /eqP ->]; rewrite all_zeroE /=. by case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)