proposition: Lemma log2_aux_matches : forall count n, n <= count -> log2_prop n (log2_aux n count).
proof: Proof. induction count. intros. assert (n = 0). auto with arith. subst. simpl. auto. intros n Hn. destruct n. simpl; auto. destruct n. simpl; auto. simpl. apply log2_prop_p. intro; discr. intro H; discr. apply IHcount; eapply Nat.le_trans. eapply le_n_S; apply div2_le_n. apply le_S_n; hyp. Qed.
imports: Coq(Lia PeanoNat) CoLoR(LogicUtil NatCompat)