proposition: Lemma Zmult_Sm_Sn : forall m n : Z, ((m + 1) * (n + 1))%Z = (m * n + (m + n) + 1)%Z.
proof: Proof. intros. ring. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)