proposition: Lemma add_list_carry_empty_neutral_n_r: forall (a: list bool) n, (n >= (length a))%nat -> (add_list_ingr a (mk_list_false n) false) = a.
proof: Proof. intro a. induction a as [ | a' xs IHxs]. - intro n. rewrite add_list_ingr_l. reflexivity. - intros [ | n]. + simpl. intro H. contradict H. easy. + simpl. intro H. case a'; apply f_equal; apply IHxs; lia. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance