proposition: Lemma exact_log2_spec : forall p i: positive, exact_log2 p = Some i -> p = (2 ^ i)%positive.
proof: Proof. induction p. - simpl; discriminate. - intro i; destruct p. + destruct p; discriminate. + case_eq (exact_log2 (xO p)). * intros p0 H H0; generalize (exact_log2xOx0 _ _ H); intro H1. generalize (IHp _ H); intro H2; rewrite H0 in H1; injection H1; rewrite H2; intro; subst i. repeat rewrite Pos_pow_power. rewrite Pos2Nat.inj_add. rewrite power_of_plus. replace (2%positive ^ Pos.to_nat 1)%M with 2%positive by reflexivity. rewrite Pos.mul_xO_r. now rewrite Pos.mul_1_r. * cbn; destruct p. destruct (exact_log2 p~1); discriminate. destruct (exact_log2 p~0); discriminate. discriminate. + cbn; injection 1;intro; now subst i. - discriminate. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)