proposition: Lemma add_to_cons a n b: b < phi0 a -> cons a n zero + b = cons a n b.
proof: Proof. by case: b => // u v w; rewrite phi0_lt1 /= => h; rewrite h (T1lt_anti h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)