proposition: Lemma lowbit_is_trunc : forall v : BV, v <> nilbv -> consbv (lowbit v) nilbv = truncbv v 1.
proof: Proof. simple induction v. intro. absurd (nil <> nilbv); unfold not in |- *; auto with arith. intros. simpl in |- *. rewrite (trunc_O bool). trivial with arith. Qed.
imports: BV Adder Gt