proposition: Lemma add_neg_list_carry_false: forall a b c, add_list_ingr a (add_list_ingr b c true) false = add_list_ingr a (add_list_ingr b c false) true.
proof: Proof. intro a. induction a as [ | a xs IHxs]. - simpl. auto. - case b as [ | b ys]. + simpl. auto. + case c as [ | c zs]. * simpl. auto. * simpl. case_eq (add_carry b c false); intros r0 c0 Heq0. case_eq (add_carry b c true); intros r1 c1 Heq1. case_eq (add_carry a r1 false); intros r2 c2 Heq2. case_eq (add_carry a r0 true); intros r3 c3 Heq3. case a, b, c; inversion Heq0; inversion Heq1; inversion Heq2; inversion Heq3; rewrite <- H2 in H4; rewrite <- H0 in H5; inversion H4; inversion H5; apply f_equal; try reflexivity; rewrite IHxs; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance