proposition: Lemma twos_complement_cons_false: forall a, false :: twos_complement a = twos_complement (false :: a).
proof: Proof. intro a. induction a as [ | a xs IHxs]; unfold twos_complement; simpl; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance