proposition: Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (inject_Z n / inject_Z m).
proof: Proof. Proof with simpl; try reflexivity. unfold Qfloor. intros. simpl. destruct m... rewrite Zdiv_0_r. rewrite Zmult_0_r... rewrite Zmult_1_r... rewrite <- Zopp_eq_mult_neg_1. rewrite <- (Z.opp_involutive (Zpos p)). rewrite Zdiv_opp_opp... Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List