proposition: Lemma lowbit_is_abit : forall v : BV, v <> nilbv -> consbv (lowbit v) nilbv = abit v 0.
proof: Proof. intros. unfold abit in |- *. unfold elemlist in |- *. rewrite strip_O. apply lowbit_is_trunc. exact H. Qed.
imports: BV Adder Gt