proposition: Lemma add_neg_list_carry_neg_f: forall a, (add_list_ingr a (map negb a) false) = mk_list_true (length a).
proof: Proof. intro a. induction a as [ | a xs IHxs]. - simpl. reflexivity. - simpl. case_eq (add_carry a (negb a) false); intros r0 c0 Heq0. rewrite add_carry_neg_f in Heq0. inversion Heq0. rewrite IHxs. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance