proposition: Lemma quots_spec (x y : Z) : ((x = -4611686018427387904 /\ y = -1 /\ quots x y = -4611686018427387904) \/ ((x <> -4611686018427387904 \/ y <> -1) /\ quots x y = Z.quot x y))%Z.
proof: Proof. unfold quots; case andb eqn: eq_min_m1. - now left; rewrite Bool.andb_true_iff, !Z.eqb_eq in eq_min_m1. - now right; rewrite Bool.andb_false_iff, !Z.eqb_neq in eq_min_m1. Qed.
imports: ZArith Sint63 ZifyBool