proposition: Lemma BV_full_adder_sum_sym : forall (v w : BV) (cin : bool), BV_full_adder_sum v w cin = BV_full_adder_sum w v cin.
proof: Proof. simple induction v. simple induction w. auto. intros. rewrite BV_full_adder_sum_eq2. rewrite BV_full_adder_sum_eq3. rewrite H. auto. simple induction w. intro. rewrite BV_full_adder_sum_eq2. rewrite BV_full_adder_sum_eq3. rewrite H. auto. intros. repeat rewrite BV_full_adder_sum_eq4. rewrite H. do 2 rewrite full_adder_carry_sym1. do 2 rewrite full_adder_sum_sym1. auto. Qed.
imports: BV FullAdder