proposition: Lemma add_list_carry_empty_neutral_r: forall (a: list bool), (add_list_ingr a (mk_list_false (length a)) false) = a.
proof: Proof. intro a. rewrite add_list_carry_empty_neutral_n_r; auto. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance