proposition: Lemma add_simpl2 n b a' n' b': a' != zero -> cons zero n b + cons a' n' b' = cons a' n' b'.
proof: Proof. by case: a'. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)