proposition: Lemma Zdiv_pos_nonneg : 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, Z.le, Z.ge in |- *; simpl in |- *; intros H0 H1; (try discriminate; auto); ( try elim H1; auto). Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)