proposition: Lemma log_of_exp2_0 : forall n p, n = exp2 p -> log2 n = p.
proof: Proof. intro n; functional induction (log2 n). - induction p;simpl; try discriminate. intro H; case_eq (exp2 p). intro H0; destruct (exp2_positive p);auto. intros n H0;rewrite H0 in H;discriminate. - destruct p. + auto. + simpl. intro H. case_eq (exp2 p). * intro H0; destruct (exp2_positive p);auto. * intros n H0; rewrite H0 in H. exfalso; lia. - intros p H; destruct p. + simpl in H; subst n; contradiction. + simpl in H; rewrite (IHn0 p); auto. rewrite H; generalize (div2_double (exp2 p));auto. Qed.
imports: Arith ArithRing Lia Recdef