proposition: Theorem log2_domain_invert : forall x:nat, log2_domain x -> x <> 0 -> x <> 1 -> log2_domain (div2 x).
proof: Proof. intros x h; case h. - intros h1 h2; elim h2; reflexivity. - intros; assumption. Defined.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9