proposition: Theorem log2_fix_eqn: forall n, log2 n = match n with 0 => 0 | 1 => 0 | S (S p) => S (log2 (div2 (S (S p)))) end.
proof: Proof. intros n; unfold log2; case (log2_terminates n); case n. - intros v [p Heq]; rewrite <- (Heq (S p) log2); auto. - intros n'; case n'. + intros v [p Heq];rewrite <- (Heq (S p) log2); auto. + intros n'' v [p Heq];case (log2_terminates (div2 (S (S n'')))). intros v' [p' Heq']; rewrite <- (Heq (S (S (p + p'))) log2), <- (Heq' (S (p + p')) log2); auto. lia. lia. Qed.
imports: Arith ArithRing Lia Wf_nat