proposition: Lemma log2_domain_non_zero : forall x:nat, log2_domain x -> x <> 0.
proof: Proof. induction 1. - discriminate. - generalize (div2_le x); intro;lia. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9