proposition: Lemma div_quots (x y : int) : to_Z (x / y) = quots (to_Z x) (to_Z y).
proof: Proof. unfold quots; destruct andb eqn: eq_min_m1. - rewrite Bool.andb_true_iff, !Z.eqb_eq in eq_min_m1. change (-4611686018427387904)%Z with (to_Z min_int) in eq_min_m1. change (-1)%Z with (to_Z (-1)) in eq_min_m1. destruct eq_min_m1 as [to_Z_x_min to_Z_y_m1]. now rewrite (to_Z_inj _ _ to_Z_x_min), (to_Z_inj _ _ to_Z_y_m1). - apply div_spec. now rewrite Bool.andb_false_iff, !Z.eqb_neq in eq_min_m1. Qed.
imports: ZArith Sint63 ZifyBool