proposition: Lemma Zmult_lt_0_reg_r_2 : forall n m : Z, 0 <= n -> 0 < m * n -> 0 < m.
proof: Proof. intros n m H1 H2;apply Z.mul_pos_cancel_r with n;trivial. Z.le_elim H1; trivial. subst;rewrite Z.mul_0_r in H2;discriminate H2. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub