proposition: Lemma add_to_cons a b c n d: d < [ a,b,c] -> cons a b c n zero + d = cons a b c n d.
proof: Proof. by case d => // u v w m z /=; rewrite psi_lt1 => h; rewrite h // (T3lt_anti h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)