proposition: Lemma limit_pr1 x: (x == zero) (+) (T2limit x (+) T2is_succ x).
proof: Proof. elim: x => //a _ b _ n c Hc /=; case az: ([a, b] == one) => //=. by case cz: (c == zero); [ rewrite (eqP cz) | move: Hc; rewrite cz]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)