fact: Definition log2_aux_F (x:nat) : (forall y:nat, y < x -> nat)->nat := match x return (forall y:nat, y < x -> nat)-> nat with | O => fun _ => 0 | S p => fun f => S (f (div2 (S p))(div2_lt p)) end.
imports: ZArith List Arith Lia Zwf Inverse_Image Extraction