proposition: Lemma add_list_carry_unit_t : forall a, add_list_ingr a (mk_list_true (length a)) true = a.
proof: Proof. intro a. induction a as [ | a xs IHxs]. - simpl. reflexivity. - simpl. case_eq (add_carry a true true). intros r0 c0 Heq0. rewrite add_carry_tt in Heq0. inversion Heq0. apply f_equal. exact IHxs. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance