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