proposition: Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b.
proof: Proof. unfold ceiling. intros a b H. apply Zdivide_mod in H. case_eq (Z.div_eucl a b). intros z z0 H0. change z with (fst (z,z0)). rewrite <- H0. change (fst (Z.div_eucl a b)) with (Z.div a b). change z0 with (snd (z,z0)). rewrite <- H0. change (snd (Z.div_eucl a b)) with (Z.modulo a b). rewrite H. reflexivity. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory