proposition: Lemma plus_inv_eq_r: forall n x y, n + x = n + y -> x = y.
proof: Proof. intros. induction n. - simpl in H. assumption. - inversion H. apply IHn. assumption. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List