proposition: Lemma phi3v a b c k: phi3 [a,b,c] k = cons a b c k zero.
proof: Proof. by elim k => // n H /=; rewrite H /= T3ltnn addn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)