proposition: Lemma BV_full_adder_sym : forall (v w : BV) (cin : bool), BV_full_adder v w cin = BV_full_adder w v cin.
proof: Proof. unfold BV_full_adder in |- *. intros. rewrite BV_full_adder_sum_sym. rewrite BV_full_adder_carry_sym. auto. Qed.
imports: BV FullAdder