proposition: Theorem log_domain_inv : forall x p:nat, log_domain x -> x = S (S p)-> log_domain (S (div2 p)).
proof: Proof. intros x p H; case H; try (intros H'; discriminate H'). intros p' H1 H2; injection H2; intros H3; rewrite <- H3; assumption. Defined.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9