proposition: Lemma Zsimpl_plus_r_dep : forall x y m n : Z, (m + x)%Z = (n + y)%Z -> x = y -> m = n.
proof: Proof. intros. apply Zplus_reg_l with x. rewrite Zplus_comm. rewrite Zplus_comm with x n. rewrite <- H0 in H. assumption. Qed.
imports: Coq(Lia)