proposition: Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
proof: Proof. unfold Qfloor. intros. simpl. destruct m as [ | | p]; simpl. - now rewrite Zdiv_0_r, Z.mul_0_r. - now rewrite Z.mul_1_r. - rewrite <- Z.opp_eq_mul_m1. rewrite <- (Z.opp_involutive (Zpos p)). now rewrite Zdiv_opp_opp. Qed.
imports: QArith