proposition: Lemma exact_log2xOx0 : forall p i, exact_log2 (xO p) = Some i -> exact_log2 (xO (xO p)) = Some (i+1)%positive.
proof: Proof. simpl; destruct p. - intro i; cbn; discriminate. - destruct (exact_log2 p~0) . + injection 1; intro; now subst i. + discriminate. - injection 1; intro; now subst i. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)