fact: Fixpoint log2 (x:nat)(h:log2_domain x){struct h} : nat := match eq_nat_dec x 0 with | left heq => False_rec nat (log2_domain_non_zero x h heq) | right hneq => match eq_nat_dec x 1 with | left heq1 => 0 | right hneq1 => S (log2 (div2 x)(log2_domain_invert x h hneq hneq1)) end end.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9