proposition: Lemma length_BV_full_adder_sum : forall (v w : BV) (cin : bool), lengthbv v = lengthbv w -> lengthbv (BV_full_adder_sum v w cin) = lengthbv v.
proof: Proof. unfold lengthbv in |- *. simple induction v. simple induction w. intros. case cin. simpl in |- *. trivial. simpl in |- *. trivial. intros. absurd (length (nil:list bool) = length (a :: l)). simpl in |- *. discriminate. exact H0. simple induction w. simpl in |- *. intros. discriminate H0. intros. simpl in |- *. rewrite H. trivial. generalize H1. simpl in |- *. auto. Qed.
imports: BV FullAdder