proposition: Theorem Zsame_sign_odiv : forall u v, (0 <= v)%Z -> (0 <= u * Z.quot u v)%Z.
proof: Proof. intros u v Hv. apply Zsame_sign_imp ; intros Hu. apply Z_quot_pos with (2 := Hv). now apply Zlt_le_weak. rewrite <- Zquot_opp_l. apply Z_quot_pos with (2 := Hv). now apply Zlt_le_weak. Qed.
imports: Coq(ZArith Lia Zquot)