proposition: Lemma limit_pr1 x: (x == zero) (+) (T3limit x (+) T3is_succ x).
proof: Proof. elim: x => //a _ b _ c _ n d Hd /=; case az: (all_zero a b c) => //. by case dz: (d == zero); [ rewrite (eqP dz) | move: Hd; rewrite dz]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)