proposition: Lemma conc1 (x:= [zero,zero, epsilon0]): limit_of (phi3 epsilon0) x.
proof: Proof. have ->: (phi3 epsilon0) = phi x. by rewrite /x phiE_3 /= /phi_rec_psi -/phi_rec_psi eqxx /=. by apply: phiL. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)