proposition: Lemma Zdiv_pos_neg : forall a b : Z, (a * b > 0)%Z -> (a < 0)%Z -> (b < 0)%Z.
proof: Proof. intros a b; induction a as [| p| p]; [ induction b as [| p| p] | induction b as [| p0| p0] | induction b as [| p0| p0] ]; unfold Z.lt, Z.gt in |- *; simpl in |- *; intros; try discriminate; auto. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)