proposition: Lemma app_lowbit_highs : forall v : BV, v <> nilbv -> appbv (consbv (lowbit v) nilbv) (highs v) = v.
proof: Proof. intros. rewrite lowbit_is_trunc. rewrite highs_is_strip. rewrite (app_trunc_strip bool). trivial with arith. exact H. Qed.
imports: BV Adder Gt