proposition: Lemma phiE_2 a b c n d: d != zero -> phi (cons a b c n d) = phi1 (cons a b c n zero) (phi d).
proof: Proof. by move => dz; rewrite phiE /phi_rec (negbTE dz). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)