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: Arith ArithRing Lia log2_it