proposition: Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.
proof: Proof. intros p x Hle;destruct (Z_le_gt_dec 0 p). apply Zdiv_le_lower_bound;auto with zarith. replace (2^p) with 0. destruct x;compute;intro;discriminate. destruct p;trivial;discriminate. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia