proposition: Lemma nat_nat_pos : forall m n : nat, ((m + 1) * (n + 1) > 0)%Z.
proof: Proof. intros. apply Z.lt_gt. cut (Z_of_nat m + 1 > 0)%Z. intro. cut (0 < Z_of_nat n + 1)%Z. intro. cut ((Z_of_nat m + 1) * 0 < (Z_of_nat m + 1) * (Z_of_nat n + 1))%Z. rewrite Zmult_0_r. intro. assumption. apply Zlt_reg_mult_l. assumption. assumption. change (0 < Z.succ (Z_of_nat n))%Z in |- *. apply Zle_lt_succ. change (Z_of_nat 0 <= Z_of_nat n)%Z in |- *. apply Znat.inj_le. apply Nat.le_0_l. apply Z.lt_gt. change (0 < Z.succ (Z_of_nat m))%Z in |- *. apply Zle_lt_succ. change (Z_of_nat 0 <= Z_of_nat m)%Z in |- *. apply Znat.inj_le. apply Nat.le_0_l. Qed.
imports: Coq(Lia)